OTS/CafeOBJ法によるマルチタスク実時間システムの形式的検証

摘要

複数のプロセスが協調して動作する実時間システムは，システムの取りうる状態数が膨大となり，安全性などの検証が容易ではない．マルチタスク実時間システムの形式的な仕様記述により，計算機支援による時間制約の形式的検証が期待される．本研究では，マルチタスク実時間システムを観測遷移システム（Observational Transition System, OTS）でモデル化し，代数仕様言語CafeOBJを用いて仕様を記述し，CafeOBJ処理系に実装されている等式推論に基づく証明スコア法でその性質を検証する手法を提案する．本手法により，複数のプロセスがそれぞれ別々の時間制約を持つようなシステムの記述が可能となる．そのようなシステムの例として，時間制約による相互排他アルゴリズム（Fischerのアルゴリズム）が任意の数のプロセスに対して相互排他性を持つことを形式的に検証する．