top of page
DynaSpecを導入するかどうかによる違い
-
アクティビティ図などのモデル図が正しく構築されているかを検証し、検証結果を可視化することで設計段階での不具合検出を助けるツールです。
-
モデル図から検証用コードを自動で生成できるため、設計者がモデルから自力でコーディングをする必要がありません。
-
検証結果はアニメーション動画で確認できるため、モデルや仕様の不具合が直感的にわかります。
DynaSpecを導入する場合
①検証用コード生成（Promelaコード変換）
②モデル検査を実行（SPIN実行・結果出力）
③検証結果を可視化
（反例アニメーション）
DynaSpecを導入しない場合
①検証用コード作成
（モデルを基に、設計者ご自身がPromelaコードを書き起こす）
②モデル検査を実行（SPIN実行・結果出力）
③出力された結果ログ
ファイルをもとに、検証結果を読み解き不具合を抽出する
SPIN結果を解析するツールを導入する。SPINについてのパラメータの意味と効果などを学習し、モデルに相応しいパラメータ設定を行う。
DynaSpecを導入しないならば、複数ツールを利用する必要があるが、DynaSpecを導入すると、一気に1つのツール上で実施できる。
結果のサマリを見ることができる。（メニュー名なんだっけ）
bottom of page