​モデルベース形式検証ツール

Q11:　形式検証を導入するにはまず何から始めればよいですか？

A11:　まずは形式検証が自社の開発のどこに適用できてどのような効果が得られるのか、

その有難さを実感して頂く必要があります。過去に後工程で不具合が顕在化した事例を

お持ちであれば、設計段階でモデル化と形式検証を導入していたら発見できていたのかを

検証するのが効果的です。ただし最初はハードルが高いと思われますので弊社では試解析

サービスを実施しております。

 

Q12:　DynaSpecは，モデルの入力値・出力値が離散値または連続値の場合，仕様の反例と

なる入力値を自動的に探索することはできますか？つまり，Falsificationできますか？

A12:　モデルの組み方次第ですが、本質的にモデル検査は反例を見つけ出すことを目的とし

ています。入力値がどの範囲の値をとり得るかを明示することで、どの値が反例に繋がるかを検出できます。

 

Q13:　形式検証では不具合の状態を定義することが必要ですが、不具合定義にも手法が

存在するのでしょうか？

A13:　不具合状態を定義するというよりは常に満たしておくべき条件を定義するイメージ

です。それを満たさない状態が検出されるとそれが不具合です。満たすべき状態は要求仕様から導き出すことになりますが、その全てを定義するのは現実的ではなく、明確な手法を

回答できませんが、形式検証で何に注目して検証したいのかの目的ははっきりさせておく

必要があります。

 

Q14:　本システム設計プロセスでの成果物は下流工程にどのように連携できるのか？　

どのツールにInput可能なのか？他社さんのツールにInputするためのI/F、APIは何か準備

されているのか？

A14:　DynaSpecを導入したとしても最終成果物は（検証済の）EAモデルになりますので、

そこからはEAの領域になります。

 

Q15:　動的にオブジェクトが複数生成されるようなモデルの検証は可能でしょうか？可能な場合どのように不具合を定義するのでしょうか？

A15:　DynaSpecでは動的オブジェク生成への対応は現時点では考慮しておりませんが、

DynaSpecではないですが、弊社の踏切モデル検査の事例では、オブジェクト（列車）最大数を予め配列で用意し、全列車共通で満たすべきASSERT条件を各オブジェクトに適用しておりました。DynaSpec上でも同じ考え方でモデル化できる可能性はあります。

 

Q16:　形式言語コードを実際の開発言語（C、C++)にどうやってコンバートするの

でしょうか？また、逆に既存のコードを取り込むことは出来ますか？

A16:　形式言語によってはC言語に変換できるものもありますし、C言語コードをそのまま

形式検証できるものもあります。DynaSpecが採用しているSPIN（Promela言語）はC言語

へのコンバート機能はありません。あくまでモデルの正しさを検証するものために形式言語へ変換するのであり、最終成果物はモデルになります。

 

Q17:　モデル検査は状態爆発で処理が終わらないという心配がありますが、どのような形でコントロールするのが良いと考えていますでしょうか。

A17:　直接的にはよりハイスペック（主にメモリサイズ）なマシン環境（最近ではAWS

環境等が利用可能）を準備することが考えられますが、これでは解決しないことが多い

です。本質的な解決策は、よりモデルを抽象化すること（本質のみに絞ってモデル化）、

検証対象を本当に評価したい範囲のモデルに絞って検証すること、1回の検証実行で全てのパターンを網羅検証するのではなく、条件の組み合わせを変えて何回かに分けて検証して

網羅性を担保すること等が考えられます。

　さらにモデルではなく形式言語に依存した対応になりますが、不要な中間状態を削減することで劇的な改善効果が得られる場合もあります。

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上でアニメーションとして可視化することも可能です。

​