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

2000 Fiscal Year Annual Research Report

• Project/Area Number: 12780206
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: 緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30272991)
• Keywords: リアクティブシステム / 仕様記述 / 検証 / 安全性 / 実時間 / 鉄道信号システム / UNITY / CafeOBJ

Research Abstract

本年度は,以下のことを行った.
・リアクティブシステムの仕様記述および検証の調査:代表的な,リアクティブシステムの仕様記述方法ならびに検証技術の調査を行った.調査した仕様記述方法・検証技術は,ChandyとMisraのUNITY,LynchのI/O Automata,MannaとPnueliの時相論理による仕様記述と検証,およびLamportのTLAである.本研究では,これらを参考に,リアクティブシステムのモデル化ならびに検証を行った.特に,本研究で用いる仕様記述言語CafeOBJとの相性のよさからUNITYを中心に用いた.
・中規模リアクティブシステムの仕様記述・検証:中規模リアクティブシステムの例として鉄道信号システムを取り上げ,UNITY計算モデル(状態遷移機械)でモデル化し,作成したモデルの仕様をCafeOBJで記述し,システムの安全性を記述した仕様を基にCafeOBJシステム支援のもとで検証を行った.検証したシステムの安全性は,「信号システムの則って列車を運行することで列車の衝突を防ぐことができる」,である.
・時間制約の導入:リアクティブシステムの仕様記述および検証の技術を応用することで,実時間システムの仕様記述および検証を行うことができる.これらの例として,AbadiとLamportのTLAを使用した実時間システムの仕様記述と検証,LynchのI/O automataを使用した方法,およびKesten,MannaおよびPnueliのCTSがある.これらを調査し,簡単な例で,CafeOBJを使って実時間システムの仕様記述と検証を行った.

Research Products

• [Publications] Seino,T.,Ogata,K.,Futatsugi,K.: "Specification and verification of a single-track railroad signaling in CafeOBJ"Proceedings of 2000 International Technical Conference on Circuits/Systems, Computers and Communications (ITC-CSCC 2000). 268-273 (2000)
• [Publications] 清野貴博,緒方和博,二木厚吉: "代数仕様言語CafeOBJによる実時間システムの仕様記述と検証-timed two-process raceの仕様記述と検証-"電子情報通信学会技術研究報告. 100・569. 17-24 (2001)