情報制御システムの分野固有の特性に基づき,段階的なモデル検査手法を開発した.従来手法より少ないメモリで検証でき,大規模モデルでは本手法の方が短時間で検証可能である.次に,システム分割によるモデル検査を可能とする分割的モデル検査手法を考案した.分割されたサブシステムの相互関係を失うことなく検証でき,無分割より短時間で検証できる.更に,両手法の欠点を解決するモジュラ検証手法を考案した.モジュラ分割を因果関係の稀薄な物理的分割,構造的対称性による分割,独立性の高い振舞いの分割という異なる3タイプの分割によるモデル検証を可能とする.この手法の効果は属性数比率により判断して利用できる.
|