2001 Fiscal Year Annual Research Report
リアクティブシステムの仕様記述、検証、および実装に関する研究
| Project/Area Number |
12780206
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30272991)
|
|---|
| Keywords | リアクティブシステム / モデル化 / 検証 / 状態遷移機械 / CafeOBJ / 実時間 / 相互排除アルゴリズム / 鉄道信号システム |
|---|
| Research Abstract |
本年度は、以下のことを行った。
・リアクティブシステムのモデル化および検証方法の整理:代数仕様言語CafeOBJおよびその実装であるCafeOBJシステムに基づくリアクティブシステムのモデル化および検証方法を整理、提案した。モデル化は、UNITY等で用いられている状態遷移機械を使って行い、作成したモデルをCafeOBJで記述し、モデルが望ましい性質を有する事をCafeOBJシステム支援のもとで行う。この方法に則り、以下のような事例研究を行った。
・分散相互排除アルゴリズムの検証:リアクティブシステムの代表例である分散相互排除アルゴリズムを例に提案方法の有効性を示した。解析したアルゴリズムは、Ricart, AgrawalaアルゴリズムとSuzuki, Kasamiアルゴリズムである。
・時間システムの分散実検証:実時間システムを扱えるように、提案方法を拡張した。有効性を示すため、鉄道の踏切り制御システム等の検証を行った。
・鉄道信号システムの検証:提案方法の有効性を示すため、2種類の鉄道信号システムを検証した。
|
Research Products
(6 results)
-
[Publications] 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)
-
[Publications] 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)
-
[Publications] 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)
-
[Publications] 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)
-
[Publications] 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)
-
[Publications] 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)
