Dynaspec の機能
Dynaspecは、UML/SysMLモデリングの標準ソフトであるEnterprise Architect（以下、EA）のアドインツールです。
EA上で作成したアクティビティ図などのモデル図が正しく構築されているかを検証し、検証結果を可視化することで、設計段階での不具合検出を助けます。
モデル図から検証用コードを自動で生成できるため、設計者がモデルから自力でコーディングをする必要がありません。
検証結果はアニメーション動画でわかりやすく可視化されるため、モデルや仕様の不具合が直感的にわかります。
EA＋Dynaspecによるモデル検査は、以下のような流れとなります。
-
EA上でUML/SysMLを使ってモデル図の作成（設計）を行う
-
Dynaspecでモデル図の検証を行う
-
①作成したモデル図を読みこみ、検証用コード（Promera）を自動生成
-
②検証用コードをモデル検査ツール（SPIN）で実行し、モデルが正しく構築されているかを検証する
-
③検証結果をアニメーションで確認し、UML/SysMLモデルや仕様の不具合箇所を特定する
-
-
EA上でUML/SysMLモデル図の不具合個所を修正する
①モデルが正しいか検証（Promelaコード変換＋SPIN実行）
-
ユーザが作成したUML/SysMLのモデル図から、検証用コード(Promelaコード)を自動生成する機能です。
-
Promelaコードは、モデル検査ツール（SPIN）を実行するための特殊なコードです。
-
モデル図から検証用コードを自動で生成できるため、設計者がモデルから自力でコーディングをする必要がありません。
-
モデル検査ツール（SPIN）実行機能は、検証用コードを使用してモデルの正しさを検証する機能です。
-
モデルが想定通りに構築できているか、前提となる仕様に不具合（望ましくない状態に到達する可能性）が含まれないかを検証することができます。
-
検証の結果を分かりやすくメッセージ表示します。不具合が見つかった場合、望ましくない状態に到達するルートを示すCSVファイルが出力されます
モデル検査を実施
（SPIN実行）
②検証結果を可視化（反例アニメーション）
-
モデル検査の結果として得られたファイル（反例CSVファイル）を可視化します。
-
元のUML/SysMLモデル上に、変数の状態遷移の変化がアニメーション表示されます。
-
ユーザはテキストベースの結果ファイルを自力で解読することなく、アニメーションから直観的に不具合箇所を見つけ、UML/SysMLを修正することができます。
-
上記の繰り返しで、不具合のないUML/SysMLモデルを作れます。
対応ダイアグラム
DynaSpecは、現在以下のUMLSysMLダイアグラムに対応しています（随時拡張中）。
-
UML構造図のクラス図、オブジェクト図
-
UML振る舞い図のアクティビティ図、ステートマシン図
-
SysMLのブロック定義図、アクティビティ図、ステートマシン図
-
振る舞いモデル検査が目的であるため、振る舞いに関するダイアグラムが中心となります。
-
入れ子構造や関数呼び出し、複数プロセスによる非同期処理の定義にも対応しています。