2020年11月13日及び11月20日に開催致しました「モデルベース形式検証による設計品質向上オンラインセミナー」（セミナー詳細について、下記リンクよりご確認くださいhttps://kke.lmsg.jp/v2/seminar/11672/CjUiirPB）ではQ＆Aセッションを設け、視聴者様から頂いた質問に講演者より回答させて頂きましたが、当日回答できなかった質問も含め、代表的な質問と回答をピックアップして以下に公開させて頂きます。

Q1:　EAは既に導入しているのですが、既存のモデルをそのままDynaSpecで検証することはできるのでしょうか？

A1:　UMLやSysMLは記述の自由度が高いために、企業によって、また人によって記述方法が異なります。また、モデル検査を行うために追加しなければならない情報(検証対象に対する外部環境やassert文の定義など)も存在します。このため、ツールを使用する上ではある程度のルールに沿ってモデルを記述する必要がありますが、DynaSpecではなるべくモデルを修正する手間が省けるように、ユーザビリティの向上に随時取り組んでおります。ご試用の上、使い勝手に関するフィードバックを頂ければ、可能な限り対応していきたいと考えております。

Q2:　興味はあるのですが、導入のプロセスがイメージできません。どのように段階的に導入すれば良いのかなどのモデルケースはありますか？

A2:　まずはお客様における過去トラを題材として試解析を実施し、実際にモデル検査を導入することが効果があること、を実感して頂くことをお勧めしております。これを行うことにより、実際に導入のイメージも掴めて来ると思います。

Q3:　DynaSpecではモデルから検査コードを自動生成するとのことですが、逆に検査コードから状態遷移図等のモデルを作ることはできるのでしょうか？

A3:　対象システムのコードから状態遷移図を生成する機能は備わっておりません。

Q4:　システムレベルというより、部品サプライヤーレベルで、より詳細ソフトウエアレベルでも活用できますか？

A4:　DynaSpecの適用対象は必ずしもシステムレベルに限定されません。大規模システムの詳細ソフトウェアレベルの設計情報をそのままモデル化すると、状態爆発の可能性がありますが、検証対象の限定やモデルの抽象度を上げることによって、適切にモデル検査を実施することが可能です。

Q5:　状態爆発について質問です。DynaSpecで状態爆発が発生しないモデルのボリュームが知りたい。例えば、入力信号の数、状態の数、状態遷移の数で答えていただければいいと思います。感覚論で大丈夫です。

A5:　状態の数や状態遷移の数だけでは一概に状態爆発の可能性を推量することは困難ですが、仮に状態爆発が発生したとしても、所与のメモリ空間内で探索を行うことにより、人手では発見しにくい不具合を抽出することが可能です。また「全網羅探索」することにより重きを置いた検証を置きたい場合には、モデルの抽象化、分割検証など様々なノウハウを以て検証することも可能です。モデル化に関するトレーニングを実施することも可能ですので、製品のご購入時に必要に応じてご要望ください。

Q6:　導入して成果がでるまでの期間はどの程度でしょうか？

A6:　一概に申し上げるのは難しいですが、ツールご購入後にまず2日程度の定型のトレーニングの実施を推奨しております。これに加えて、導入をよりスムーズに行うためにお客様のご要望に即した個別トレーニングや導入コンサルティングも実施しており、これは数カ月単位を想定しております。

Q7:　形式検証で不具合として発見できる現象は、どのような種類があるのでしょうか？逆に、形式検証/モデル検査では発見しにくい不具合というのはあるでしょうか？ある場合はどういったものが発見しにくいといったことがあれば教えて頂ければと思います。

A7:　まずモデル検査の適性が高いシステムは基本的には離散系システムです。このようなシステムにおいて発見できる不具合の例としては、セミナーでもご紹介差し上げた「モードの不整合」のような不具合が挙げられます。モデル検査を適用する際にはAssert条件として「満たすべき事象」を定義する必要がありますが、この「満たすべき事象」を離散変数の論理式で表現できるようなシステムであれば、どのような不具合でも抽出可能です。

Q8:　SysML等のモデリングの支援もされていますでしょうか

A8:　形式検証を行う上で必要となるモデリングのトレーニングを行っております。

Q9:　検出された不具合はどのような形式で出力されるのでしょうか？

A9:　不具合が抽出されたこと、また、不具合を抽出するのに要したメモリ等の情報はテキストファイルで出力します。また、不具合が発生した場合に、その不具合に至るログ情報についてはcsv形式で出力します。このログ情報をEA上でアニメーションとして可視化することも可能です。