プログラムスライシングによるプログラムのモデル検査手法
スポンサーリンク
概要
- 論文の詳細を見る
プログラムの動作を検証し, 信頼性を保証することは重要である. 検証したいプログラムを状態遷移システム上で定義し, モデル検査を行うことは可能だが, OSのようにその規模が大きく動作が複雑な場合そのままモデル検査を行うのは現実的ではない. 本論文ではプログラムスライシング技術を用いたプログラムの自動検証手法を提案する. Cプログラムのソースからプログラムスライシングにより特定の処理に関する部分のみを抽出し, それから状態遷移システムを構成して自動検証を可能にする. 最後に検証ツールSMVを用いての検証について説明する.
- 2001-05-21
著者
関連論文
- プログラムスライシングによるプログラムのモデル検査手法
- 演繹的モデル検査による自動詳細化検証手法
- 文字の位相表現について
- OSスケジューラプログラムの自動検証の実験的研究
- 制御ソフトウェアの開発方法論 : 制御理論と計算機科学の横断的設計アプローチ
- E-commerceソフトウェアの形式的開発方法論
- Assume-Guarantee形式による実時間ソフトウェアの演繹的詳細化検証手法
- 実時間システムの演繹的検証と自動検証の実験的研究
- 実時間システムの演繹的検証