SATソルバーとソフトウェア検証技術（その4）
皆さま、こんにちは。
IDAJの小川です。
今回も前回を踏まえて、モデル検査を活用するアイディアについてご説明します。
モデルのリファクタリング
皆様は既存のモデルに対して、既存の振る舞いを保ったまま何らかの機能を追加しなければならなかったり、モデルの構造を振る舞いを変更せずにより単純化したい（リファクタリング）と思われたことはないでしょうか？
では、既存のモデルの振る舞いを完璧に保持したまま、モデルの構造をブラッシュアップできるという自信はあるでしょうか？
自慢ではありませんが・・・私はありません！（苦）
既存のモデルに何らかの変更を加える場合には慎重にならざるをえません。
往々にして、ちょっとした変更が既存のモデルの振る舞いを変えることがあるからです。
そこで、ぜひモデル検査をご活用ください！
既存モデルと編集後のモデルが一致することをモデル検査で確認することで、自信を持ってモデルのリファクタリングができるようになります。
ここでは以下の図に示すような状態遷移系を題材に考えていきたいと思います。
このSCADE言語の状態遷移系では、太い黒枠で示されたinitが開始時の状態ですが、initからの遷移条件がtrueに設定されている（常に遷移が発生するようになっている）ために実際にはアクティブにならず、1ステップ目の状態は必ずStateAもしくはStateBになります。
その後、StateAもしくはStateBにとどまり続けます。
モデルとしては単純なものですが、この例のinitのように、絶対にアクティブにならない状態は、モデルの構造として考えたときには冗長です。
特にSCADE言語の場合、状態遷移系内の各状態に対してアクティブになることがモデルカバレッジ基準として要求されているため、絶対にアクティブにならない状態はテストケースによってモデルカバレッジを達成することができません。
SCADE言語のように、ソフトウェアの振る舞いを記述するモデリング言語には、”テストケースによってモデルのデータフローや制御フローがどの程度観測されたか？”を評価する”モデルカバレッジ”と呼ばれる指標が存在します。
ソースコードの構造カバレッジに類似した考え方に基づく指標ですが、一般的にはモデルカバレッジと、そのモデルから生成したソースコードの構造カバレッジは一致しません。
しかしSCADE言語モデルの場合は、モデルカバレッジを達成しておけば、モデルから生成したコードの構造カバレッジも自動的に達成されることが保証されています。
では、この状態遷移系を、アクティブにならない状態が存在しないように構造を変更してみましょう。
まず、元のモデル”Operator_Before”をコピーして”Operator_After”とし、コピー後のモデルを修正していきますが、修正を始める前に、Operator_BeforeとOperator_Afterの出力が常に等しいという性質を検証する検査モデルを以下のように作成しておきます。
モデル検査をすると、現時点では検査結果は当然Validとなります。
なお、今回の例では出力が1つだけなので、1つの出力結果の比較結果を検査していますが、出力を複数持つモデルの場合にはそれぞれに対応する出力を比較した結果の論理積を検査することになります。
続いて、Operator_Afterを変更します。
まずは冗長な状態であるinitを削除します。そしてStateBを初期状態とした上で、Input1がtrueの時にStateBからStateAに遷移する遷移条件を定義してみましょう。
Operator_BeforeもInput1がtureの時にStateAへ遷移し、falseの時にStateBへ遷移するので、何となくこれでよさそうに思えます。いかがでしょうか？
そこで、先ほどのモデル検査を実行してみると、残念ながら反例が出力されました。
出力された反例をシミュレーションしてみると、ステップ目ではInput1=falseが入力され、Operator_Before/AfterともにStateBへ遷移していますが、次の2ステップ目でInput1=trueとすると、Operator_Afterの方はStateAへの遷移が発生しています。
これを踏まえてStateBがアクティブになった後は、StateAへの遷移が発生しないよう、モデルの構造を変更します。
Signalは、StateBがActiveの時にはtrue、そうでない時にはfalseとなるローカル変数です。遷移条件にnot last ‘Signalを追加することで、前回ステップでStateBがアクティブ（=Signalがture）の時には遷移が発生しなくなります。
ここで再度モデル検査を実行してみると、今度はValidとなりました。
これで冗長な状態を削除した状態遷移系へのリファクタリングが無事完了です。
このように、モデル検査で確認しつつモデルを変更していくことで、思わぬ考慮漏れを回避しながらも、モデルのリファクタリングを確実に進めることができるようになります。
その他の活用方法 ～テストケースの生成～
テストケースの生成にもモデル検査を活用することができます。
モデルカバレッジを達成するためのテストシナリオを検討しているとき、例えば”Output_AとOutput_Bが 同時にtrueになるようなテストシナリオが欲しいけれど、なかなか作成することができない・・・”ということがあります。
こんなときは、”Output_A=true かつ Output_B=true”をあえて否定した性質が常に満たされるかどうかをモデル検査してみます。この時、もし反例が得られれば、それが”Output_A=true かつ Output_B=true”となるテストシナリオの例となります。
少々逆説的ですが、このように”ある性質を否定した性質を検査する”ことで、もとの性質を満たす具体例を取得するという活用方法が考えられます。
本連載の表題であるSATソルバーから離れた話題が続いてしまいましたが、最後にSATソルバーならではの話題として”数独”をご紹介したいと思います。
数独とは3×3のブロックに均等に分割された9×9のマトリクスのセルに、1~9の数値を以下のルールで入力していくパズルです。
- マトリクスの各行には1~9の数値は1回しか出現しない（必ず1回だけ出現する）
- マトリクスの各列には1~9の数値は1回しか出現しない（必ず1回だけ出現する）
- 3×3のブロックには1~9の数値は1回しか出現しない（必ず1回だけ出現する）
こうしたパズルもSATソルバーを使用することで解くことができます。
次回は世界一難しい部類とされる以下の数独を、SCADEのモデル検査を使って解いてみましょう！
【出典】https://rocketnews24.com/2012/07/03/22654/
本記事の内容にご興味がおありの方は、詳細のご説明や資料提供、各ソリューションのデモが可能ですので、ご遠慮なく弊社営業担当(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