OSスケジューラプログラムの自動検証の実験的研究
スポンサーリンク
概要
- 論文の詳細を見る
OSなどのリアクティブシステムを検証し, 信頼性を保証することは重要である.しかし, 従来の研究では, 状態遷移システムや抽象化されたプログラムの検証に留まっており, プログラムの論理的動作などの検証が出来ない.本論文ではリアクティブシステムの操作的意味を状態遷移システムで形式化する立場より, OSスケジューリングプログラムの自動検証手法を提案する.リアクティブシステムのデータ領域を抽象化することにより, 有限な状態遷移システムを構成して, 自動検証を可能にする.最後に検証ツールSMVを用いた検証により, その有効性を示す.
- 社団法人電子情報通信学会の論文
- 2000-05-12
著者
関連論文
- プログラムスライシングによるプログラムのモデル検査手法
- 演繹的モデル検査による自動詳細化検証手法
- OSスケジューラプログラムの自動検証の実験的研究
- 制御ソフトウェアの開発方法論 : 制御理論と計算機科学の横断的設計アプローチ
- E-commerceソフトウェアの形式的開発方法論
- Assume-Guarantee形式による実時間ソフトウェアの演繹的詳細化検証手法
- 実時間システムの演繹的検証と自動検証の実験的研究
- 実時間システムの演繹的検証