(形式的仕様)振舞い近似手法を用いたステートチャートに対する不変性の検証(<特集>オブジェクト指向技術)

概要

論文の詳細を見る
本稿では,互いに依存する複数のステートチャートを合成することなく不変性の検証を行う手法を示す.単一のステートチャートの検証では,まず最初に与えられたステートチャートをステートチャートに対する正規表現に変換する.そして,本稿で提案する形式的体系を用いて,Hoareのプログラム検証手法と同じ方法を用いて不変性に関する検証を行う.振舞いが互いに依存する複数のステートチャートの検証においては,通常は合成と呼ばれる手法が用いられる.しかし,状態爆発などの問題を起こすため,本稿では合成後に得られるステートチャートの振舞いに徐々に近づける手法を提案する.この方法は,目的とする検証が行えるようになるまで何度でも適用できる.また,ステートチャートどうしの通信方法には様々ある.ステートチャートがどのように協調動作するのかに応じて,ステートチャート間の通信方法を決める必要がある.そこで,提案する手法では,通信方法に応じて柔軟に対応できるようにしている.
一般社団法人情報処理学会の論文
2003-06-15