モデル検査
モデル検査
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2018/10/03 20:59 UTC 版)
「Guarded Command Language」の記事における「モデル検査」の解説
ガード付きコマンドは Promela というプログラミング言語で使われている。Promela はSPINモデルチェッカで使われている。SPINは並行ソフトウェアアプリケーションのモデル検査用ツールである。
※この「モデル検査」の解説は、「Guarded Command Language」の解説の一部です。
「モデル検査」を含む「Guarded Command Language」の記事については、「Guarded Command Language」の概要を参照ください。
モデル検査
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2018/10/21 06:03 UTC 版)
本来、モデル検査はモデルが仕様を満足するかを検証する技法として開発された。モデルベーステストに応用する場合、テスト対象システムのモデルとテストしたい属性をモデル検査機に与える。モデル検査機はその属性がモデル上で正しいかどうかを証明する過程で証拠と反例を検出する。証拠となる経路はその属性を満足する。一方、反例となる経路を実行すると、その属性に反した状態となる。これらの経路がテストケースとして使用できる。
※この「モデル検査」の解説は、「モデルベーステスト」の解説の一部です。
「モデル検査」を含む「モデルベーステスト」の記事については、「モデルベーステスト」の概要を参照ください。
ウィキペディア小見出し辞書の「モデル検査」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。 お問い合わせ。
モデル検査と同じ種類の言葉
- モデル検査のページへのリンク
