コンカレントシステムの仕様検証手法

概要

論文の詳細を見る
離散事象システムの検証にとっては, 可達性の検証が有効とされているが可達性の確認は計算量的に不可能であるといわれている. それは, 現状の可達性解析が状態木を生成するという総当たり的な手法をとっていることによる. しかし, カオス理論に見られるように, 見た目上は複雑で解析できそうもないものであっても, 自然界の法則に従うものの中には, 単純な数個の解析し易いものの組合せである場合があり, 簡単に解析できる場合もあることがわかってきている. また離散事象システムの挙動によっては複雑で解析できそうにないものでも, 簡単な状態の組合せで表すことができ, さらに状態を発散する場合でもある規則に従う場合がある. 本稿では, その離散事象システムの持つ規則を導きだし, それを利用する状態生成手法を提案する. さらに, 本手法は状態遷移木を作成する状態生成手法より低コストの計算量で行なえることを離散事象システムの一つである通信システムを例に提案する.
社団法人電子情報通信学会の論文
1997-07-11