Formal Verification パッケージ

BTC EmbeddedPlatformの形式検証は、検証対象のソフトウェアが要求に違反しないことを「証明 」します。

Formal Verification パッケージ

BTC EmbeddedPlatformのFormal Verification パッケージは、モデルチェック(Model Checking)と呼ばれる静的解析技術を用いた形式検証をサポートしています。TargetLink モデルまたはCコードのの振る舞いに要求違反が存在しないことを数学的に証明します。もし要求違反に到達し得る場合には確実に検出して要求違反の再現環境を提示します。

モデルチェックによる形式検証は非常に強力なテクノロジです。テストケースを書く必要は無く、カバレッジも測定する必要はありません。シミュレーションを用いた如何なるテストよりも網羅度の高い検証結果をもたらします。これだけ魅力的であるにも関わらず、このテクノロジの実用は敬遠される傾向にありました。利用に高度な専門的知識と技術を要するものであったためです。BTC EmbeddedPlatformにおいてはその限りではありません。最低限の操作でどなたでもご利用いただける直感的なユーザインタフェースが準備されています。ユーザ様には量産開発に適用できる実用的な形式検証としてご評価いただいています。

 

Formal Verificationパッケージ

サポートするユースケース

*1 Formal Specificationパッケージの機能はすべて含まれます。

追加可能なアドオン

 

モデルチェックによる形式検証

モデルベース開発では、モデルを用いてソフトウェアの設計が行われます。このときモデルは要求群に基づいて設計されます。すなわち、原則としてモデルは要求群に違反してはなりません。モデルの要求違反不在を数学的に証明できる検証手法がモデルチェックによる形式検証です。

モデルチェックでは、検証対象のモデル(またはコード)に生じ得る全ての可能な入力値とその組み合わせを無限の時間に対して網羅的かつ自動で評価します。ありとあらゆる実行が評価されるため、ソフトウェアが要求に違反しないことを数学的に証明することができます。また、要求違反に到達し得る場合には必ず検出して要求違反の再現環境を提示します。

 

(本動画の前半はフォーマルテストの紹介です。後半がモデルチェックによる形式検証の紹介となっております。)

 

モデルチェックによる形式検証の対象

機能モデル (TargetLinkモデル)

ソフトウェア機能モデルのモデリング及びシミュレーションにはMathworks社のSimulinkが広く活用されています。BTC EmbeddedPlatformのモデルチェックによる形式検証では、Simulink上で動作するdSPACE TargetLinkのブロックセットで構成されたソフトウェアの機能モデルを検証の対象としています。

一般的に機能モデルのテスト・検証にはModel-in-the-loop(MIL)シミュレーションと呼ばれるSimulinkのモデルシミュレーション機能が用いられますが、モデルチェックによる形式検証では静的な解析を行うため、デバッグの際に要求違反の原因解析を除いてMILシミュレーションは用いません。

実装モデル (TargetLinkモデル)

機能モデルに対し、実装用のデータタイプやスケーリング、クラスやストレージといった情報が追加され、必要に応じて一部のブロックを実装用に差し替えたものが実装モデルです。実装モデルは一般的に自動コード生成機能を持つツールを用いて作成されます。BTC EmbeddedPlatformのモデルチェックによる形式検証では、TargetLinkブロックセットで構築された実装モデルにおけるデータタイプやスケーリングを考慮します。これは、最終実装で利用される現実的な値に範囲を絞ることで検証の高速化を行うためです。クラスやストレージは基本的に考慮しません。(クラスやストレージはBack-to-backテストで評価されます。)

一般的に実装モデルのテスト・検証には、機能モデルのときと同じくModel-in-the-loop(MIL)シミュレーションと呼ばれるSimulinkのモデルシミュレーション機能が用いられますが、モデルチェックによる形式検証では静的な解析を行うため、デバッグの際に要求違反の原因解析を除いてMILシミュレーションは用いません。

ソースコード (Cコード)

実装用のソースコード(Cコード)はdSPACE社のTargetLink、Mathworks社のEmbedded Coderといった自動コード生成ツールによって自動的に生成されます。

一般的にCコードのテスト・検証には、Visual StudioやMinGWといった汎用コンパイラを用いたSoftware-in-the-loop(SIL)シミュレーションが用いられますが、モデルチェックによる形式検証では静的な解析を行うため、デバッグの際に要求違反の原因解析を除いてSILシミュレーションは用いません。

BTC EmbeddedPlatformを用いたモデルベース開発において、機能モデル(もしくは実装モデル)が十分にテスト・検証されている場合、ソフトウェアユニットレベルのソースコードの検証はBack-to-backテストで行われることが多いため、モデルチェックによる形式検証を適用する必要性は高くありません。

 

完全な検証

BTC EmbeddedPlatform上の形式検証ではありとあらゆる実行が評価されるため、ソフトウェアが要求に違反しないことを数学的に証明することができます。これはすなわち、検出漏れは生じ得ないことを意味します。例えば、製品が想定外の利用方法で使われた、緊急時用の機能が正常時に誤って動作してしまう、要求に関係ないと思っていた信号が実は間接的に影響していた、機能が複数回利用された後にだけ正常に動作しなくなる、といった原因に由来する要求違反は、従来のテスト手法では検出を確実にすることは困難です。想定されていない問題をピンポイントで検出するようなテストケースを作成することは非常に困難であるためです。形式検証ではこういった見落としの可能性を完全に排除することができます。

 

テストケース不要、カバレッジ不要

ありとあらゆる可能な入力値とその組み合わせを無限の時間に対して網羅的かつ自動で評価するため、テストケースは一切記述する必要がありません。カバレッジ測定してテスト品質を評価する必要もありません。

テストケースを記述する工数、レビューする工数は全く必要無くなります。

 

単純明快な操作と検証結果

BTC EmbeddedPlatform上の形式検証は極限まで自動化されているため、要求の形式化さえ行ってしまえば後の操作は極めてシンプルです。数回のクリックのみで形式検証の実行を行うことができます。また、レポートされる結果も基本的に要求を満たす(Fulfilled)、要求に違反する(Violated)のいずれかのみです。(解析のタイムアウトやPCのリソース不足によるエラーが無い場合に限ります。)

 

デバッグし易い要求違反例の提示

形式検証によって要求違反が検出された場合、要求違反を再現するデバッグ環境が提供されます。デバッグ環境はSimulink上で実行可能なモデル、またはVisual Studio上で実行可能なCコードです。ユーザはデバッグ環境上で1ステップずつ、演算の中間値を観測しながらシミュレーションすることで、要求違反に至った経緯を分析することができます。このとき、長いシミュレーションを経てようやく要求違反に辿り着くような要求違反例が与えられていると、デバッグ作業は非常に複雑かつ難解なものになります。BTC EmbeddedPlatformの形式検証では、常に要求違反に到達する最短の要求違反例を提示することで、デバッグの効率を上げています。

また、BTC EmbeddedPlatformの提示する要求違反例では、各ステップでの要求の状態変化がレポートされます。この要求の状態変化とデバッグ環境のモデル(もしくはコード)の状態を照らし合わせることで、デバッグをさらに容易に行うことができます。

 

モデルチェックによる形式検証の自動化

モデルチェックによる形式検証は要求毎に実行されます。MATLABスクリプトなどを用いて連続実行すれば解析は昼夜を問わず継続されることから、エンジニアの方々の貴重な工数は要求違反が検出された場合のデバッグに集中することができます。

 

要求の形式化

要求の形式化はUniversal Patternを用いて行います。Universal Patternは直感的かつ可読性の高いグラフィカルな形式言語です。形式手法の専門知識が無い方でも簡単に読み書きすることができます。形式化という言葉に構える必要はありません。

要求の形式化について、詳しくは要求記述と形式化をご参照ください。

 

各種機能安全規格準拠 

BTC EmbeddedPlatformのモデルチェックによる形式検証は、各種機能安全規格の最新版に準拠し、 ドイツTÜV Süd社による認証を受けています。

 

 

要求の形式化分の作業が追加されたとしても効率は上がる?

はい、要求の形式化の作業が追加されたとしても、形式検証を用いれば効率向上が期待できます。

要求の形式化さえ完了してしまえば、後の操作は簡単で、テストケースを書く必要が一切なく、カバレッジを測定する必要もなく、効率的なデバッグ環境まで提供されます。従来のテスト・検証において最も工数を必要とする作業の多くが省かれるため、大きな工数削減をご期待いただけます。

 

どの程度の規模まで適用可能?

形式検証は強力な検証テクノロジではありますが、検証対象規模には制約があります。制約は単純なモデルの大きさだけでなく、要求の複雑さ、PCの性能にも依存するため、単純に表すことは困難ですが、経験上大体ソフトウェアユニット程度の規模です。余りに規模の大きな解析では、状態爆発と呼ばれる状態に陥り、検証結果を得るのに非常に時間がかかる、PCのリソースが不足するなどの問題を生じる恐れがあります。

 

Requirements-basedテスト、フォーマルテストよりもモデルチェックによる形式検証の方が良い?

Requirements-basedテスト、モデルチェックによる形式検証、フォーマルテストは要求に基づいたテスト・検証を行うという観点では同じですが、いずれにも長所短所があるため、一概にどれが良いとは言えません。どれかを選択するよりも、用途に合わせて使い分けることの方が重要です。一つの開発プロセス上でも適切に組み合わせて利用することによって効率的かつ効果的なテストプロセスを構築することが可能になります。比較と使い分けの詳細はこちらをご覧ください。