並行システム記述におけるフォールトパターンに関する考察

摘要

モデル検査では，デッドロックや仕様が満たされないことを検出した場合，反例が提示ざれるが，その原因となるフォールトの特定は困難な作業である．本研究では，並行システムを状態遷移機械の集合と捉え，典型的なフォールトをパターンとして定義する．検証前にフォールトに成り得る箇所を指摘することにより検証コストの削減を図る．