SATソルバーとソフトウェア検証技術（その1）
皆さま、こんにちは。
IDAJの小川です。
今回から5回にわたって、「SAT（サット）ソルバーを用いたソフトウェアの検証技術」についてご紹介したいと思います。
SATソルバーとは？
突然ですが皆さまは、「SATソルバー」という言葉をご存じでしょうか？
SATソルバーの”SAT”とは、”boolean SATisfiability problem”、すなわち 与えられた命題論理式が真になるかどうかを判定する充足可能性判定問題を意味しています。
A and (not B)
という命題論理式は、”A=true, B=false”のときに”true”となるため、充足可能な命題論理式です。
SATソルバーとは、充足可能性判定問題の解を探索するための専用のソルバー（プログラム）のことです。
SATに関しては、「計算機科学のノーベル賞」とも言われるチューリング賞の受賞者であり、組版システムTeXの開発者としても有名な数学者・計算機科学者であるDonald E. Knuth氏が、大著”The Art of Computer Programming”の中で
SAT is evidently a killer app, because it is key to the solution of so many other problems.
と述べています。その中で、実に300ページ近い分量がSATの説明に充てられている（Volume 4 Fascicle 6, Satisfiability, 2015）ことからも、その重要性は推して知ることができます。
SATは計算量的にNP完全とよばれるクラスの問題に属することが証明されており、効率的に解を求めることが難しい問題とされていますが、一方で2000年以降SATソルバーの性能が飛躍的に進化し、様々な応用が進んでいます。
私たちの身近（？）なところでは、ソフトウェアの検証技術、例えば自動テスト生成や（有界）モデル検査に応用されています。
モデル検査とは?
「シフトレフト」が叫ばれる中、開発の上流段階で様々な”モデル”が活用されるようになっています。
“モデル”とは、着目したい性質などの分析対象のある側面を表現したものです。
ソフトウェア開発においてもシステムのアーキテクチャやソフトウェアの振る舞いを表現したモデルが作成され、開発要件の把握やモデルシミュレーション、モデルからの自動コード生成等を通じ、開発のフロントローディングや開発プロセスの自動化に活用されています。
“モデル検査”とは、モデルが所定の性質を満たすかどうかを、数学的な手法でモデルを解析することによって検証する手法の総称です。
“数学的な手法でモデルを解析する”の意味ですが、これは”検査対象とするモデルに対して何らかの検証アルゴリズム=形式的（formal）な手続きを適用する”ということを意味しています。
上述したSATをベースとした（有界）モデル検査では、通常いわゆる「状態遷移系」で表現されるモデルを 検証の対象とするため、検査対象となるモデルは、検証アルゴリズムで解析可能な状態遷移系に変換できる必要があります。
SATベースの（有界）モデル検査イメージとしては、初期状態から開始して、kステップ以下の遷移により到達可能な各状態において性質Pの 否定 が成立するかどうか（以下のような命題論理式が充足可能かどうか）を、SATソルバーにより探索します（あくまでもイメージです）。
もしSATソルバーにより解が見つかれば、性質Pが満たされない例（性質Pの反例）が探索できたことになります。
またもし解が見つからない場合には、初期状態からkステップ以前の各状態では性質Pが常に成立することを数学的に検証できたことになります。
モデル検査を活用するには？
一般的にモデル検査は、活用するに至るまでの障壁が高いと言われています。
その理由として、数理論理学等の数学的な手法に立脚しているために”とっつきにくい”ことが挙げられることが時々あります。
確かに、モデルが所定の性質を満たすかどうかを検証するアルゴリズムそのものを詳細に理解することは容易ではありません。
しかし、実際には、検証アルゴリズムを実装した検証エンジンを活用するために必要な、モデルが満たすべき性質の記述方法などの論理学の知識を得るために、数理論理学や数学基礎論の専門書を読破する必要は全くなく、少々のトレーニングによって習得することが十分可能なのです。
むしろモデル検査活用のネックとなっているのは、検証エンジンに入力可能な形式でモデルを用意するのが難しいという点にあると思います。
ソフトウェア開発の現場で活用されている各種のモデルのデータは、そのままではモデル検査の検証エンジンへの入力として直接には指定できないことが多く、検証エンジンによって要求される所定の書式に変換する必要があります。
またモデルを検証エンジンへの入力とする仕組みが構築されている場合でも、モデルの解釈を一意的に確定して数学的な解析を可能とするために、モデルに対して何らかの制約を課す必要がある場合もあります。
このような障壁を回避して
- 作成したモデルに対して直接モデル検査を適用し、検証が実行できたら？
- さらに検証済みのモデルからソースコードを自動的に生成できたら？
より効率的で品質の高いソフトウェア開発が可能となるに違いありません。
モデル検査を身近に実現するAnsys SCADE
これらを実現できるソフトウェア開発環境として、弊社ではクリティカルなシステム・ソフトウェアの統合開発環境Ansys SCADEをご提供しています。
Ansys SCADEは「機能安全認証に対応したモデルベース開発環境」で、グラフィカルな表示を持つモデリング言語であるSCADE言語を用いて、ソフトウェアの振る舞いを定義するモデルを作成し、シミュレーションによる挙動の確認からソースコードの自動生成を行うことができます。
Ansys SCADEは機能安全認証に対応したモデルベース開発環境です
特長的なのが、SCADE言語自体が構文論と意味論が厳格に定義された形式言語であること、そして自動コード生成機能が機能安全認証規格に準拠して開発されており、モデルと自動生成コードの振る舞いが一致することをツール側で保証している点です。それによって、モデルレベルの検証活動のみで、自動生成コードに対するコードレビューや単体テスト、Back-to-Backテスト、コードカバレッジ解析を省略することができます。
モデルと自動生成コードの整合性
Ansys SCADEに関する詳細については、是非過去のブログ記事もご参照ください。
関連ブログ（記事）
認証取得済みコード生成機能を核とした、組み込みソフトウェアのモデルベース開発環境「AnsysSCADE」 のご紹介（その1）
認証取得済みコード生成機能を核とした、組み込みソフトウェアのモデルベース開発環境「Ansys SCADE」 のご紹介（その2）
認証取得済みコード生成機能を核とした、組み込みソフトウェアのモデルベース開発環境「Ansys SCADE」 のご紹介（その3）
これによって、Ansys SCADEでは、SCADE言語モデルに対して十分な検証を実施しておくことによって、最終的な成果物であるソースコードを自動的に生成することが可能になります。
そして、モデルレベルでの検証活動をサポートする機能として、Ansys SCADEではSATソルバーをベースとしたモデル検査による検証機能が提供されており、任意のSCADE言語モデルに対して簡単にモデル検査を実行することが可能となっています。
次回はAnsys SCADE環境におけるモデル検査の具体的な実施イメージについてご紹介したいと思います。
本記事の内容にご興味がおありの方は、詳細のご説明や資料提供、各ソリューションのデモが可能ですので、ご遠慮なく弊社営業担当(info@idja.co.jp)までご連絡ください。
無料オンラインセミナー（Webinar）
弊社では、Ansys SCADEにご興味のあるお客様を対象に、常設で下記のオンラインセミナーを開催しています。
「開発責任者・管理職・シニアエンジニア様向けAnsys SCADEご紹介セミナー」
本セミナーでは、普段、Ansys SCADEを操作されることはなくても、組み込みソフトウェア開発を統括・推進されている開発責任者・管理職・シニアエンジニアの皆様に、Ansys SCADEがどのようなシーンでお役に立つのかをわかりやすくご説明しています。IDAJは単にソフトウェアのご提供だけでなく、機能安全規格に準拠した開発プロセスへのツール適用や効率的なモデルの作成などをコンサルティングサービスとしてご提供します。ぜひご都合の良い時間にご視聴いただければ幸いです。
追記・更新：2021年5月27日
■オンラインでの技術相談、お打合せ、技術サポートなどを承っています。下記までお気軽にお問い合わせください。ご連絡をお待ちしています。
株式会社 IDAJ 営業部
Webからのお問い合わせはこちら
E-mail：info@idaj.co.jp
TEL： 045-683-1990