CafeOBJ 仕様変換器 C-TRAS を用いた検査法

4.4. CAFEOBJ仕様変換器C-TRASを用いた検査法

図

4.15: C-TRAS

を用いた検査法のフロー図

4.4. CAFEOBJ仕様変換器C-TRASを用いた検査法

1)

仕様中の軽微な誤りの場合，反例より容易に仕様が修正できる．修正後，再び も出る検査を行う．

2)

仕様中の重大な誤りの場合，反例よりその原因を特定し仕様の修正を試みる．

この作業は困難であり，誤りを修正した仕様を作成できないかもしれない．

3)

実現不能な問題をとこうとしている場合．仕様の修正を繰り返しても，反例を 取り除くことはできない．

1, 2

の場合，反例より仕様の修正が容易になる ．反例が自動で得られることか ら，証明論敵手法に比べ早期に誤りを発見し，修正することができる．

•

反例が発見されない場合，その原因は二つ考えられる．

1)

制限によって切り捨てた状態遷移機械に反例が含まれている．

2)

振舞仕様に誤りが存在しないため，モデル検査で反例が得られない．

制限によって得られた

SMV

仕様では誤りが無いことを示すことはできない．こ のためより強い確信を得たい場合は，制限を緩め再びモデル検査を行う．十分 な確信が得られた時点で，CafeOBJ検証器による検証に切り替える．

• CafeOBJ

検査器による検証

無限状態に対する証明はモデル検査器では直接行う事ができない．このため

CafeOBJ

を用いて検証を行う．証明論的手法による検証は，公理と仕様から証明できること は限られており，多くの場合 検証の途中で定理を追加する必要がある．

定理を追加するためには，その定理が成り立つことを振舞仕様上で成り立つこと を証明しなければならない．この作業は容易ではなく，検証者の能力に大きく依存 する．しかしモデル検査によって定理の証明を支援することができる．定理の候補 をモデル検査で検証することにより，誤りのある定理候補の証明を試みる事が無く なる．定理を証明するために別の定理が必要になることもあり，モデル検査によっ て候補を絞って検証できることは能率的な検証に大きく貢献する．

振舞仕様に対しモデル検査技術を適用することは，制限情報を与えること以外，自動で 行う事ができる．また誤りがある場合に反例を示すことができる点で

CafeOBJ

による検 証を支援することができる．

両者を併用して検証を行うことにより，誤りの発見と仕様の修正・検証を機械と人で分 担し，検証を能率良く行う事が期待される．

第 5 _章

例題

本章ではいくつかの例題に対し

C-TRAS

を利用してモデル検査を行う事で，事前検査 の有効性を確かめる．

ドキュメント内 JAIST Repository (ページ 59-62)