論文：要求分析段階におけるモデル検査技術を用いた設計制約検証の自動化
本日はこちらです。最近個人的な流行りの、要求分析段階におけるモデル検査の話です。
まとめると、
・複数機器の通信等による同期ズレがよく発生する
・UMLのフロー、シグナル送受信をモデル検査することで設計制約を満たすことを検証する
・有効性をシステム事例で確認する
ということです。
例によって気になった箇所を引用します。
モデル検査ツールUPPAAL
初めて聞きました。
スウェーデンの会社みたいですね。有償か…。astahは持っているのですが、UPPAAL前提だときついですね。SPINとかでできないんだろうか。おそらくGUIで状態遷移モデルを表現してくれる点が強いのかな、とも思いました。
UMLは、自然言語を用いてシステムの流れを自由に、静的に記述することができる
自然言語前提でしたっけ…。まぁ確かにモデリングとはいっても、自然言語が含まれない、を意味するわけではなく、部分的に形式化されているだけ、なんですよね。あと「静的」にももやもやするものがありますが置いておきましょう。
モデル検査技術は、システムの振る舞いを有限状態遷移図に表し
モデル検査の中に状態遷移が多いことは知っていますが、すべてが状態遷移なのでしょうか。モデル検査という言葉なので、いろんなモデルが対象になってしかるべきかなとは思いますが、現状状態遷移モデルぐらいしか対象にできないということでしょうか。
表1 モデル要素の対応
アクティビティ図と状態遷移図の対応付けをしてくれているので手元で確認ができそうですね。UPPAALは使いたくないですが…。
今後の課題は、UPPAALモデルに変数を加え、事前条件、事後条件による各フローのつながりを追えるようにすることである
正直何が現状足りてなくて、何が困っているのかが理解できてないんですよね。そもそものモデル検査についての知識が足りないんです。。うーん、家にある「SPINによる設計モデル検証」を読む時が来ましたかね。