分散システムのための代数仕様記述と検証に関する研究

2000 Fiscal Year Annual Research Report

• Project/Area Number: 11780207
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: 森 彰 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30311682)
• Keywords: 分散システム / 振舞仕様 / 隠蔽代数 / 安全性 / モデル検査 / 無限状態 / 定理証明

Research Abstract

今年度の研究の目的は,前年度の研究で発見された安全性モデル検査手続きに厳密な定式化を与え,これをセキュリティや実時間システムの問題に適用できるよう,新たな仕様記述の仕組みを明らかにすることであった.安全性モデル検査については,隠蔽代数を用いて記述された分散システムの振舞仕様を(無限)状態遷移機械の定義とみなし,システムの状態を隠蔽ソート上の述語として表現する述語抽象の考え方を定式化するに至った.これによって,プログラム検証において扱われて来た述語変換の手法が利用できるようになり,モデル検査とプログラム検証の関係が明らかになった点が意義深いものであった.この述語変換を用いた最小不動点の繰り返し計算として安全性モデル検査を定式化し,定理証明を用いた述語間の含意証明による収束判定を用いた繰り返し手続きとして簡潔な定義を与えることができた.そして,代数仕様システムCafeOBJ上で新たに自動定理証明器PigNoseを開発し,このモデル検査手続きを利用できるようにした.ユーザーはCafeOBJによる仕様と検査したい安全性述語を定義するだけでよく,他の類似システムにあるような構文変換や時相論理式による検証条件の記述が不要であることから,無限状態システムを対象としたモデル検査器として他に類をみないものとなった.さらに移動コードの仕様を,コード実行の操作的意味と安全性検査機構をまとめた抽象機械として定義することで,どのようなコード体系であっても安全性検査が可能であるとの知見を得た.実時間システムにおいては,大域時間を示す属性と時間進行のための操作を定義し,状態変化に伴い最大遅延や最小遅延といった時間制約の属性をセットすることで,安全性が検査できることが確認できた.また本研究では,仕様記述とその検証に同一の論理体系が用いられていることから,対話的検証に対する有効性も確認することができた.

Research Products

• [Publications] 森彰: "開放型分散環境でのソフトウェア部品検証システムの研究開発"第19回IPA技術発表会論文集. 27-35 (2000)
• [Publications] Joseph Goguen: "An Overview of Tatami Project"CAFE : An Industiral-Strength Algebraic Formal Method. 61-78 (2000)