ハイブリッドモデルによる組込みシステムの高信頼性設計方法論の構築と支援環境の開発

2003 Fiscal Year Annual Research Report

• Project/Area Number: 14580368
• Research Institution: Kanazawa University
• Principal Investigator: 山根 智 金沢大学, 工学部, 教授 (70263506)
• Keywords: ハイブリッドモデル / 組込みシステム / 詳細化検証 / 仕様記述 / 定理証明 / 確率 / 模倣検証

Research Abstract

本年度は、前年度の基本検討を踏まえて、以下の研究を行なった。
(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)

Research Products

• [Publications] 山根 智, 中村一博: "実時間システムのための近似手法に基づいた記号モデル検査器の開発と評価"電子情報通信学会. J86-D1,No.3. 232-247 (2003)
• [Publications] Satoshi Yamane: "Formal refinement verification method of real-time systems with discrete probability distributions"2nd International Workshop on Automatic Verification of Infinite-State Systems. 2. 202-215 (2003)
• [Publications] 山根 智: "離散確率分布を持つリアルタイムシステムの詳細化検証手法"情報処理学会論文誌. 44,8. 2189-2199 (2003)
• [Publications] Satoshi Yamane: "Deductive Schedulability Verification Methodology of Real-Time Software using both Refinement Verification and Hybrid Automata"Porceedings of IEEE 27th COMPSAC. 27. 527-533 (2003)
• [Publications] Satoshi Yamane: "Probabilistic Timed Simulation Verification and its application to Stepwise Refinement of Real-Time Systems"Lecture Notes in Computer Science. 2896. 276-290 (2003)
• [Publications] Satoshi Yamane: "Deductive Verification of Probabilistic Real-Time Systems"Proceeding of IEEEThird International Workshop on Assurance in Distributed Systems and Networks. 3. 33-37 (2004)