実践！ソフトウェアモデル検査

■ 実用化の研究

モデル検査用語辞典

■ モデル

モデルとはシステムの設計書、仕様書から作成する模擬システムです。モデル検査専用言語を用いて作成します。通常のプログラミング言語と同様に簡単なコーディングによって作成することができます。

■ モデル検査器

モデル検査器とはモデルと検査項目を入力すると計算機上でモデル検査を自動的におこなうソフトウェアツールです。当研究会ではモデル検査ツール NuSMV を使用しています。
NuSMVはイタリアで開発されたフリーのソフトウェアツールです。

■ 検査項目

モデル検査で作成したモデルに対して、検証したい性質や項目を記述します。検査項目は、時相論理式を用いて作成します。

■ 時相論理式

命題論理式に時間の概念を取り入れた論理式になります。命題論理式では、ある状態の真偽しか記述することができませんが、時相論理式ではある状態から次状態でどう変化したか、いつまでその状態が成り立つかを記述することができます。

オンラインサービス

支援ソフトウェア

Copyright(C) 2005-2011 Practical research group of Software Model checking. All Rights Reserved.