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

点击翻译按钮获取中文摘要

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