タイマを用いる有限状態機械でモデル化されたシステムの検証手続き
スポンサーリンク
概要
- 論文の詳細を見る
本論文ではタイマを用いる有限状態機械モデルで記述されたシステムに対する検証手続きについて議論する.検証はタイマと有限状態機械からなる系における到達可能な状態の列挙に基づいて行われる.しかしタイマの設定時間が大きい場合, 到達可能な状態数が膨大となるため, 到達可能な状態を列挙するにはメモリや計算時間の点で問題となる.そこでタイマの取り得る値を連立不等式を用いて表し, 複数の状態と状態遷移を一括して扱い到達可能な状態を列挙する手法を提案した.また提案手法による到達可能な状態の列挙に基づく検証手続きを実装し, DHCPに適用した.その結果, DHCPの到達可能な状態を現実的な時間で列挙し, タイマと有限状態機械間のやりとりに不具合がないことを検証することができた.
- 一般社団法人情報処理学会の論文
- 2001-02-20
著者
-
樋口 昌宏
大阪大学大学院基礎工学研究科
-
樋口 昌宏
近畿大学理工学部
-
谷口 健一
大阪大学 基礎工学部
-
谷口 健一
大阪大学大学院情報科学研究科
-
森 亮憲
大阪大学大学院基礎工学研究科
-
徳田 康平
大阪大学大学院基礎工学研究科
-
樋口 昌宏
近畿大学 理工学部 情報学科
-
谷口 健一
大阪大学 大学院基礎工学研究科 情報数理系専攻
-
徳田 康平
大阪大学 大学院基礎工学研究科 情報数理系専攻
-
森 亮憲
大阪大学 大学院基礎工学研究科 情報数理系専攻
関連論文
- データ付時間オートマトンの双模倣等価性の記号的検証法
- 外部入力値のみを保持できる整数変数をもつFSMに対する記号モデル検査法(ソフトウェア工学)
- 通信プロトコルのエラーリカバリ性自動検証の一方式
- 拡張時間オートマトン群による実時間システムの記述および検証
- 遷移条件が状態訪問回数に依存する有限状態機械対からなる通信系の生存性検証
- 時間制約を保証するUML/OCLを用いた分散実時間アプリケーション開発手法(ソフトウェア,フォーマルアプローチ論文)
- UML/OCLを用いた分散実時間アプリケーション開発手法の提案
- UML/OCLを用いた分散実時間アプリケーション開発手法の提案
- D-3-6 分散実時間アプリケーションのUML/OCL記述から時間オートマトンネットワークを用いた動作仕様記述への変換手法の提案(D-3. ソフトウェアサイエンス, 情報・システム1)
- 分散環境実時間アプリケーション開発支援のためのTimeliness QoS一貫性検証系および時間制御コード生成系の実装