SATソルバーとソフトウェア検証技術（その2）
皆さま、こんにちは。
IDAJの小川です。
前回はSATソルバーとSAT（サット）ソルバーをベースとしたモデル検査の概要、そしてモデル検査を身近に実現する開発環境としてAnsys SCADEについてご紹介しました。
今回はAnsys SCADEにおけるモデル検査の実施イメージについてご説明します。
モデル検査の手順は大きく4つの段階にわけられます。
- 検査対象モデルのモデリング
- 検証する性質の記述
- モデル検査の実行
- 検証結果の解析
1. 検査対象モデルのモデリング
最初のステップはモデル検査を適用させる詳細設計モデルの作成です。
Ansys SCADEではSCADE言語を使用してモデルを作成することになりますが、言語といっても以下の図のように、グラフィカルなエディタ上でソフトウェアの振る舞いを定義することができます。
ここではクルーズ制御のモデルを例として作成しています。アクセルペダル、ブレーキペダルと車速の情報と制御指令に対して、巡航車速とスロットル開度、クルーズ制御の状態を出力します。
モデル検査の実践 ～モデリング～
2. 検証する性質の記述
次のステップは検証する性質の記述です。
Ansys SCADEでは検証する性質についてもSCADE言語で記述し、モデルとして作成します。ここでは検証する性質を表現するためのモデルを「性質モデル」と便宜的に呼ぶことにします。
先ほどのクルーズ制御モデルの場合、例えば”Cruise ControlがONでないときは、スロットル開度とアクセルペダルは同じでなければならない”という性質は以下のようなモデルで表されます。
verif::impliesというブロック（operator）は、1番目の入力をA、2番目の入力をBとしたときに
“AならばB”が成立するときには”true”、成立しない時には”false”
を出力します。
では”ブレーキが踏まれたら、クルーズコントロールはinterruptedもしくはOFFにならなければならない”という性質はどうでしょう？
これをSCADE言語を使って性質モデル化するには、”ブレーキが踏まれたら”という自然言語で記述された曖昧な条件を明確にして形式的に表現しなければなりません。それが明確になって初めて、性質モデルを記述することができるのです。
ここでは”Brake > PedalsMin(=3%)”を”ブレーキが踏まれた”状態だと定義して、以下のような性質モデルを作成してみました。
このように、モデル検査に当たっては、検査する性質を形式化して表現することが要求されます。
自然言語の曖昧な表現や未定義用語による説明の考慮不足をごまかすことができませんので、モデル検査の実行過程で”仕様の検証”という副次的な効果が期待できます。
モデル検査の実践 ～性質の記述～
3. モデル検査の実行
性質モデルの記述が完了したら、詳細設計モデルと性質モデルを組み合わせて、詳細設計モデルの入出力に対して性質モデルの出力が常にtrueになるかどうかをチェックする 「検査モデル」を作成し、モデル検査を実行します。
また、モデル検査時に入力の範囲を限定したい場合には、Assertion/Guaranteeによって検査モデルに制約を設定するという仕組みがSCADEには用意されています。
今回のクルーズ制御の例では、Assertionの設定によりSpeed（車速）を0~150[km/h]、AccelとBrakeを0~100[%]の範囲に限定しました。
Ansys SCADEのモデル検査の実行手順そのものはとても簡単で、検査モデル上の出力に対してProof Objectiveを右クリックで挿入した後、挿入したProof objectを右クリックで[Analyze]とします。
実行が終了すると、常に検証対象の性質が満たされる場合にはValid、そうでない場合にはFalsifiableと表示されます。
モデル検査の実践 ～モデル検査実行～
4. 検証結果の確認
検証結果がFalsifiableとなる場合には、検証対象の性質が満たされなくなる状態に至る反例シナリオが出力されますので、反例シナリオを検査モデル上にロードしてシミュレーションを実行し、不具合発生要因を解析します。
今回の場合、”ブレーキが踏まれたら、クルーズコントロールはinterruptedもしくはOFFにならなければならない”という要件に対して、ブレーキペダルが踏まれた状態であるにもかかわらず、スタンバイ状態への予期せぬ遷移が発生しているため、遷移条件の見直しが必要であることがわかります。
このようにモデル検査は、性質の完全検証にはもちろん有効ですが、提示された不具合シナリオの解析によって詳細設計モデルの品質向上にも役立てることができ、特にテストシナリオが作りにくい複雑な条件分岐や状態遷移の検証に威力を発揮します。
モデル検査の実践 ～不具合の検証～
以上がAnsys SCADE上でモデル検査を実施する場合の概略です。
詳細設計モデルの作成は別として、モデル検査そのものはほぼクリック操作のみで容易に実行開始できることがご理解いただけたかと思います。
また生成される反例もモデル上でグラフィカルに1ステップずつシミュレーションできるため、どのような経路で性質が満たされなくなるのかを視覚的にわかりやすく確認することができます。
次回はモデル検査を更に活用する方法について見ていきたいと思います。
本記事の内容にご興味がおありの方は、詳細のご説明や資料提供、各ソリューションのデモが可能ですので、ご遠慮なく弊社営業担当(info@idja.co.jp)までご連絡ください。
Ansys SCADEに関する詳細については、是非過去のブログ記事もご参照ください。
関連ブログ（記事）
認証取得済みコード生成機能を核とした、組み込みソフトウェアのモデルベース開発環境「AnsysSCADE」 のご紹介（その1）
認証取得済みコード生成機能を核とした、組み込みソフトウェアのモデルベース開発環境「Ansys SCADE」 のご紹介（その2）
認証取得済みコード生成機能を核とした、組み込みソフトウェアのモデルベース開発環境「Ansys SCADE」 のご紹介（その3）
無料オンラインセミナー（Webinar）
弊社では、Ansys SCADEにご興味のあるお客様を対象に、常設で下記のオンラインセミナーを開催しています。
「開発責任者・管理職・シニアエンジニア様向けAnsys SCADEご紹介セミナー」
本セミナーでは、普段、Ansys SCADEを操作されることはなくても、組み込みソフトウェア開発を統括・推進されている開発責任者・管理職・シニアエンジニアの皆様に、Ansys SCADEがどのようなシーンでお役に立つのかをわかりやすくご説明しています。IDAJは単にソフトウェアのご提供だけでなく、機能安全規格に準拠した開発プロセスへのツール適用や効率的なモデルの作成などをコンサルティングサービスとしてご提供します。ぜひご都合の良い時間にご視聴いただければ幸いです。
■オンラインでの技術相談、お打合せ、技術サポートなどを承っています。下記までお気軽にお問い合わせください。ご連絡をお待ちしています。
株式会社 IDAJ 営業部
Webからのお問い合わせはこちら
E-mail：info@idaj.co.jp
TEL： 045-683-1990