リアクティブシステムの仕様記述、検証、および実装に関する研究

2001 年度 実績報告書

• 研究課題/領域番号: 12780206
• 研究機関: 北陸先端科学技術大学院大学
• 研究代表者: 緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30272991)
• キーワード: リアクティブシステム / モデル化 / 検証 / 状態遷移機械 / CafeOBJ / 実時間 / 相互排除アルゴリズム / 鉄道信号システム

研究概要

本年度は、以下のことを行った。
・リアクティブシステムのモデル化および検証方法の整理:代数仕様言語CafeOBJおよびその実装であるCafeOBJシステムに基づくリアクティブシステムのモデル化および検証方法を整理、提案した。モデル化は、UNITY等で用いられている状態遷移機械を使って行い、作成したモデルをCafeOBJで記述し、モデルが望ましい性質を有する事をCafeOBJシステム支援のもとで行う。この方法に則り、以下のような事例研究を行った。
・分散相互排除アルゴリズムの検証:リアクティブシステムの代表例である分散相互排除アルゴリズムを例に提案方法の有効性を示した。解析したアルゴリズムは、Ricart, AgrawalaアルゴリズムとSuzuki, Kasamiアルゴリズムである。
・時間システムの分散実検証:実時間システムを扱えるように、提案方法を拡張した。有効性を示すため、鉄道の踏切り制御システム等の検証を行った。
・鉄道信号システムの検証:提案方法の有効性を示すため、2種類の鉄道信号システムを検証した。

研究成果

• [文献書誌] K.Ogata, K.Futatsugi: "Specifying and verifying a railroad crossing with CafeOBJ"Proc. of the the 15^<th> Int l Prallel, Distributed Processing Symposium(IPDPS O1). 150-150 (2001)
• [文献書誌] K.Ogata, K.Futatsui: "Formally modeling and verifying Ricart&Agrawala distributed mutual exclusion algorithm"Proc. of the Second Asia-Pacific Conference on Quality Software(APAQS 01). 357-366 (2001)
• [文献書誌] K.Ogata, K.Futatsugi: "Modeling and verification of distributed real-time systems based on CafeOBJ"Proc. of the 16^<th> IEEE Int l Conference on Automated Software Engineering(ASE 01). 185-192 (2001)
• [文献書誌] K.Ogata, K.Futatsugi: "Formal analysis of Suzuki&Kasami distributed mutual exclusion algorithm"Proc. of the IFIP TC6/WG6.1 Fifth Int l Conference on Formal Methods for Open Object-Based Distributed Systems. (2002)
• [文献書誌] T.Seino, K.Ogata, K.Futatsugi: "Specification and verification of tokenless blocking systems with CafeOBJ"Proc. of the 2001 Int l Technical Conference on Circuits/Systems, Computers and Communications. 807-811 (2001)
• [文献書誌] T.Seino, K.Ogata, K.Futatsugi: "Specification and verification of a single-track railroad signaling in CafeOBJ"IEICE Transactions on Fundamentals of Electronics, Communications and Computer Science. E84-A・6. 1471-1478 (2001)