| 研究概要 |
本年度は、前年度の基本検討を踏まえて、以下の研究を行なった。
(1)モジュール単位のハイブリッドシステムが仕様記述可能な計算モデルである、フェーズ遷移モジュールを基礎とした支援環境を実現して、リアルタイムオペレーティングシステム及びリアルタイムソフトウェアを仕様記述して、詳細化検証を行って、評価して、その実用性を実証した。その成果を国際会議で発表した。
(Satoshi Yamane : Deductive Schedulability Verification Methodology of Real-Time Software using both Refinement Verification and Hybrid Automata、Porceedings of IEEE 27th COMPSAC)
(2)ランダム性のあるリアルタイムハイブリッドシステムを対象として、新たな仕様記述言語と詳細化検証の公理系を開発した。その成果を国際会議などで発表した。
(Satoshi Yamane : Probabilistic Timed Simulation Verification and its application to Stepwise Refinement of Real-Time Systems'', LNCS 2896, Springer-Verlag)
(3)さらに、(2)を拡張して、無限な対象を有する、ランダム性のあるリアルタイムハイブリッドシステムを対象として、新たな仕様記述言語と演繹的な詳細化検証の公理系を開発した。その成果を国際会議で発表した。
(Satoshi Yamane : Deductive Verification of Probabilistic Real-Time Systems'', Proc. IEEE Third International Workshop on Assurance in Distributed Systems and Networks)
|
