SATソルバーとソフトウェア検証技術（その3）
皆さま、こんにちは。
IDAJの小川です。
前回は、Ansys SCADEでモデル検査を実行するときの手順をご紹介しましたが、SCADE言語の場合は、任意のモデルに対してモデル検査を実行することができるため、検証する性質をSCADE言語で記述してしまえば、“モデル検査を実行すること”そのものはとても簡単です。
モデル検査と状態爆発
ところで、モデル検査には”状態爆発”という弱点があることをご存じでしょうか？
状態爆発とは、「検査すべきモデルの状態遷移の組み合わせが膨大になり、モデル検査を実行開始したはいいものの、いつまでたっても検査が終わらない」という問題で、残念ながらAnsys SCADEのモデル検査でも状態爆発の発生自体を回避することはできません。
モデル検査の状態爆発が発生した場合の回避方法の1つが“モデルの抽象化”です。例えば、外部から与えられる整数入力を
- 正、0、負の3つの状態入力とする
- 偶数、奇数の2つの状態入力とする
というように集約することで、モデルが取りうる状態数を減らす工夫をするというものです。
しかし、このモデルの抽象化によって、本来検出されるべき反例が検出されなくなったり、逆に抽象化後のモデルで検出された反例に対応する反例が元のモデルで存在しない”偽反例”が検出されることがあるため、問題に応じた慎重な対処が必要となります。
また、そもそも「全ての状態の網羅的な検査そのものを諦める」という考え方もあります。
これは、「完全な検証を完遂することを目的とするのではなく、”とりあえずモデル検査を実行してみて、反例が見つかったらモデルの修正等の対処を行う”というループを回すことで、モデルの品質を向上させることを優先する」という考え方です。
つまり、”多くの不具合は探索範囲が小さくても反例として発見される”という、いわゆる 小スコープ仮説(Small Scope Hypothesis) に基づくある種の”割り切り”です（※）。
（※）D. Jackson and C. A. Damon. Elements of style: Analyzing a software design feature with a counterexample detector. IEEE Transactions on Software Engineering, 1996
特にAnsys SCADEの場合は、モデル検査の実行自体は簡単で、反例もグラフィカルなモデル上でのシミュレーションによって具体的に確認できるため、このような”割り切り”による試行錯誤に対する敷居は低いのではないかと思います。
では続いて、このような”割り切り”によって、「網羅的で厳密な検証」というモデル検査ならではの特長に加えて、「品質向上のために活用できる技術」という観点からモデル検査を、実務で積極的に活用するアイディアについて見ていきたいと思います。
ちなみに、”組み合わせ爆発”がどのようなものか気になる方は、「組み合わせ爆発 おねえさん」と検索してみてください。
モデル検査によるテスト駆動開発
近年のシステム開発では、プログラムの実装前にテストコードを書き（テストファースト）、そのテストコードに適合するように実装やリファクタリングを進めていく”テスト駆動開発”が広く普及しています。
テスト駆動開発と同様の流れに沿って、Ansys SCADE上のモデル検査を用いてモデルを作成してみましょう。
題材として、有名なFizzBuzz問題を取り上げます。ここでは以下の仕様を満たす”FizzBuzzモデル”を作成します。
- 1つの8ビット符号なし整数（uint8）を入力とする（以下、Input1とする）
- Input1が3の倍数のときにはFizzを出力する
- Input1が5の倍数のときにはBuzzを出力する
- Input1が3の倍数かつ5の倍数のときにはFizzBuzzを出力する
- それ以外のときにはOtherを出力する
モデルの出力データ型は、Fizz, Buzz FizzBuzz, Otherを要素とする列挙型”tFizzBuzz”を独自定義して設定することにしました。
モデルの最初の実装は、単純にOtherを出力するだけの内容だとしておきます。何も定義しないと、Ansys SCADEではモデルの静的検証時に出力未定義エラーとなります。
次に仕様検証用（検査モデル）を作成します。最初に”3の倍数のときにはFizzを出力する”という仕様ですが、”3の倍数かつ5の倍数のときにはFizzBuzzを出力する”という別の仕様も踏まえ、以下のようにモデル化（check_Fizz）し、OutputにProof Objectiveを設定します。
同様に”5の倍数のときにはBuzzを出力する”、”3の倍数かつ5の倍数のときにはFizzBuzzを出力する”を検証するための検査モデル（check_Buzz, check_FizzBuzz）を作成し、Proof Objectiveを設定します。
この段階で一度モデル検査を実行してみましょう。現段階では、FizzBuzzモデルは常にOtherを出力するので、全ての検査結果がFalsifiableになります。ある意味当然の結果が得られることで、モデル検査が正しく機能していることを確認できます。
続いてFizzBuzzモデルを実装していきます。
入力を3、5、15で割った余りを計算(それぞれローカル変数mod_03、mod_05、mod_15に格納)し、その値に応じて出力を決定します。
“3の倍数かつ5の倍数のときにはFizzBuzzを出力する”で、再度、モデル検査を実行すると検査結果はFalsifiableとなりました。
反例を[Load Scenario]によってモデル上でシミュレーションしてみると、FizzBuzzを期待しているところで、モデルの出力がFizzになっていることがわかります。
より詳細に確認すると、255という15の倍数に対して3の倍数かどうかの判定が最初に行われていたため、結果としてFizzが出力されていたことがわかりました。
そこで、15で割った余りが0になるかどうかを最初に検証するようにモデルを変更します。
再度モデル検査を実行すると、全ての検査結果がValidとなることを確認できました。
見事、仕様を満たすFizBuzzモデルの実装完了です！
あとは、モデル検査結果がValidとなる状況を保ちつつ、モデル内部の構造をブラッシュアップ（リファクタリング）するという作業を必要に応じて実施します。
以上のように、実際のモデルを作成する前に、モデルが満たすべき仕様を検証するための検査モデルを作成しておき、モデル検査で反例が示されないようにモデル実装を進めていくことで、より効率的に不具合のないモデルを実装することができるようになります。
また、実装をブラッシュアップしてもモデル検査で反例が示される場合は、検査モデルそのもの、ひいては仕様そのものに不備があることに気づいたり、仕様そのものに対する理解を深めることができる可能性があります。
今回の例では、”Input1が3の倍数のときにはFizzを出力する”という仕様は、”Input1が3の倍数であり、かつ5の倍数ではないときにはFizzを出力する”がより厳密な仕様であるため、これを踏まえて検査モデルを作成しないとモデル検査で反例が出力され続けることになります。
一般的なテスト駆動開発では、何らかのテストフレームワークを使用してテストコードを作成することになりますが、今回の例ではテストコードの代わりにモデル検査を用いたので、実際には単純なテストよりも厳格な検証ができたことになります。
例えば”255という入力に対してFizzBuzzという期待値を検証する”という内容のテストコードを書くのと、”15の倍数に対して常にFizzBuzzという結果が返ってくることを網羅的に検査する”のとの違いです。
特にAnsys SCADEでは、モデルと生成コードの振る舞いが一致していることをツール側で保証しているため、モデル検査によって厳格に検証された性質を持つモデルから生成されたコードもその性質を満たします。そのため、上記のような”モデル検査ファースト”の開発は”証明駆動開発”に近い内容となっています。
長くなってしまったので今回はここまでとさせていただき、次回にもう少しモデル検査の活用について考えていきましょう。
本記事の内容にご興味がおありの方は、詳細のご説明や資料提供、各ソリューションのデモが可能ですので、ご遠慮なく弊社営業担当(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