| 研究概要 |
本年度は,以下のことを行った.
・リアクティブシステムの仕様記述および検証の調査:代表的な,リアクティブシステムの仕様記述方法ならびに検証技術の調査を行った.調査した仕様記述方法・検証技術は,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を使って実時間システムの仕様記述と検証を行った.
|
