Formal Test パッケージ

BTC EmbeddedPlatformのフォーマルテストは、様々なシミュレーション実行記録を解析し、要求違反やテスト漏れを自動で検出します。

Formal Test パッケージ

BTC EmbeddedPlatformのFormal Test(フォーマルテスト) パッケージは、要求に基づいたソフトウェア及びシステムのテストを自動化するための製品です。形式化された要求群に基づき、MIL、SIL、PIL、HILでシミュレーションしたありとあらゆる結果に対する判定を自動で行います。従来のRequirements-basedテストと比べて、より少ない工数でより高い質のテストが行えます。ユーザ様には、従来のテストとの相性も良く、かつ属人的なテストからの脱却を可能にするテスト技法としてご評価いただいています。

Formal Testパッケージ / Formal Test BASE パッケージ*1

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

*1 Formal Test BASEパッケージはFormal Testパッケージから自動テストケース生成機能のみを除いた製品です。

*2 Formal Test BASEパッケージには含まれません。

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

*4 Requirements-based Testパッケージの機能はすべて含まれます。

追加可能なアドオン

 

フォーマルテスト

モデルベース開発では、開発プロセスの様々な統合レベル(ソフトウェアユニットレベル、ソフトウェアインテグレーションレベル、システムレベル)で要求に基づいた検証が行われます。この要求に基づいた検証を目的として、シミュレーションと形式手法を組み合わせることで柔軟かつ高効率なテストを実現した技法がフォーマルテストです。

フォーマルテストでは、テスト対象のシミュレーション実行記録を解析し、形式化された要求群との照合を自動で行います。そしてシミュレーション実行中に要求が満たされた(Fulfilled)、要求に違反した(Violated)、もしくは要求が評価されなかった(Inconclusive)のいずれかの結果を要求毎にレポートします。BTC EmbeddedPlatform上で実行したシミュレーション実行記録は全て判定対象とできます。外部でシミュレーションした実行記録をBTC EmbeddedPlatformにインポートして判定対象とすることも可能です (オフライン フォーマルテスト)。

 

フォーマルテストのテスト対象

ECU及びシステム (ECUまたは仮想ECU)

ECU及び複数のECUで構成されたシステムの仮想実行環境として、HILを用いたシミュレーションが広く活用されています。また、仮想ECUを用いたシミュレーションも活用されています。BTC EmbeddedPlatformは特に、戦略的パートナーであるdSPACE社のSCALEXIOに代表されるHIL製品群及びVEOS、Control Desk、Automation Deskとの高い親和性を持っています。

機能モデル (Simulinkモデル/TargetLinkモデル)

ソフトウェア機能モデルのモデリング及びシミュレーションにはMathworks社のSimulinkが広く活用されています。機能モデルは、Simulinkの標準のブロックセットまたはこれに追加されたdSPACE TargetLinkのブロックセットで構成されます。

機能モデルのテスト・検証にはModel-in-the-loop(MIL)シミュレーションと呼ばれるSimulinkのモデルシミュレーション機能が用いられます。

実装モデル (Simulinkモデル/TargetLinkモデル)

機能モデルに対し、実装用のデータタイプやスケーリング、クラスやストレージといった情報が追加され、必要に応じて一部のブロックを実装用に差し替えたものが実装モデルです。実装モデルは一般的に自動コード生成機能を持つツールを用いて作成されます。自動コード生成用のツールとして代表的な製品はdSPACE社のTargetLink、Mathworks社のEmbedded Coderです。

実装モデルのテスト・検証には、機能モデルのときと同じくModel-in-the-loop(MIL)シミュレーションと呼ばれるSimulinkのモデルシミュレーション機能が用いられます。

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

実装用のソースコード(Cコード)はdSPACE社のTargetLink、Mathworks社のEmbedded Coderといった自動コード生成ツールによって自動的に生成されます。近年ではターゲットに依存しないANSI-C準拠のCコードが用いられるため、Visual StudioやMinGWといった汎用コンパイラによるSoftware-in-the-loop(SIL)シミュレーションがテスト・検証に用いられています。

BTC EmbeddedPlatformを用いたモデルベース開発において、機能モデル(もしくは実装モデル)が十分にテスト・検証されている場合、ソフトウェアユニットレベルのソースコードの検証はBack-to-backテストで行われることが多いため、フォーマルテストを適用する必要性は高くありません。一方で、ソフトウェアインテグレーションレベルのテストはモデルではなくCコードで行われることもあります。その場合はCコードもフォーマルテスト適用の対象として有効です。 

オブジェクトコード

最後にターゲットコンパイラを用いてコードのコンパイル・リンクを行い、ターゲットプロセッサ上で実行可能なオブジェクトコードを得ます。オブジェクトコードのテスト・検証には、ターゲットプロセッサを搭載した評価ボード上でシミュレーションを行うProcessor-in-the-loop(PIL)シミュレーションが用いられます。PILシミュレーションではターゲット特有の仕様や最終的に利用するコンパイラオプションも含めた評価が可能です。特に浮動小数点実装においてはターゲット依存の振る舞いに注意する必要があるため、PILシミュレーションは重要な役割を担います。

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

 

フォーマルテストで得られる結果

要求に基づいた自動合否判定

フォーマルテストでは各要求に対して、合否判定をレポートします。すべてのシミュレーション実行記録が、すべての要求の判定対象になります。したがって、テスト全体としてどの要求が満たされた(Fulfilled)、違反された(Violated)、もしくはそもそも要求が評価されなかった(Inconclusive)という結果が一目瞭然です。テスト漏れも人の目によってではなく、システマチックに検出できます。

要求カバレッジ

フォーマルテストでは、単純に各要求をテストしたかどうかの判定に留まらず、要求内の各条件に対するカバレッジも自動測定します。これは要求カバレッジと呼ばれ、要求に基づいた自動合否判定と同時に自動で測定されます。要求カバレッジを通して、各要求に対するテストケースの量と質が十分であったかを評価することができます。

要求カバレッジは後述の構造カバレッジとは異なり、ECUや仮想ECUなども含め対象を問わず測定可能です。

 

構造カバレッジ

モデルやコードを対象にする場合は、さらに構造カバレッジの測定が可能です。最も代表的な構造カバレッジはModified Condition/Decision カバレッジ(MC/DC)です。他にも、Statementカバレッジ、Branch(Decision)カバレッジ、Functionカバレッジ、Callカバレッジなどが広く活用されています。BTC EmbeddedPlatformではこれらのカバレッジを自動測定し、レポートします。

要求カバレッジに加えて、フォーマルテストに用いられるテストケースの完全性を評価する指標としてご活用いただけます。

BTC EmbeddedPlatformでサポートされたカバレッジゴール一覧

 

シミュレーション実行記録のみでの判定

 シミュレーション実行記録は必ずしもBTC EmbeddedPlatform上で取得する必要はありません。オフライン フォーマルテストと呼ばれる用法により、外部からインポートしたシミュレーション実行記録も判定の対象とすることができます。

Open-loopシミュレーション・Closed-loopシミュレーション両対応

フォーマルテストは、テスト対象のソフトウェア単体でのOpen-loopシミュレーションだけでなく、これをプラントモデルと結合したClosed-loopシミュレーションにも対応しています。

 

HILシミュレーション実行中のリアルタイム判定

アドオンであるRTT-Observerを追加すれば、シミュレーション実行記録をいったん取得してから判定するのではなく、 シミュレーション実行中にリアルタイムでフォーマルテストの判定を行うことも可能です。この手法は、dSPACE HILまたはVEOSでシミュレーションする場合のみご利用いただけます。

詳しくはアドオンRTT-Observer Generatorをご参照ください。

 

要求からのテストケース自動生成

Formal Testパッケージでは、形式化された要求からのテストケース自動生成に対応しています。この機能によるテストケース生成は、単純に各要求を網羅するだけでなく、要求カバレッジに基づいて要求内の各条件を網羅します。またこの機能では、要求を網羅する最短のテストケースが得られるため、レビューやデバッグの負担が軽減されます。

* この機能はFormal Test BASEパッケージには含まれません。

 

要求の形式化

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

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

各種機能安全規格準拠 

BTC EmbeddedPlatformのフォーマルテストは、各種機能安全規格の最新版に準拠し、 ドイツTÜV Süd社による認証を受けています。

 

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

はい、要求の形式化の作業が追加されたとしても、フォーマルテストを用いれば効率向上が期待できます。

例えば、

「車速が30km/hより遅い、または180km/hより速いときには、ACCシステムは非アクティブ化しなければならない」

という要求に対してテストを行う際に用いるテストケースは、システムの状態、境界値、要求に直接言及されていないものの関連する信号の振る舞いなどを考慮すると、多くの場合一つでは足りません。そしてそれぞれのテストケースに対して時系列の入力値と出力値(期待値)のセットを定義していく作業は一般的に大変大きな労力を要します。そして完成したテストケースが元の要求のテストとして本当に適切であったかをレビューする作業は、場合によっては作成する作業に匹敵するほどに工数を要します。

一方で、要求の形式化はそれぞれの要求に対して一回の作業です。Universal Patternを用いれば私たちの普段の用語に近い表現となり、情報量も絞られますので、数字の羅列のテストケースよりも容易にレビューできます。また要求は再利用性が高いため、差分開発などでは要求の大半を再利用することができます。

判定は全て形式化された要求に任せられるようになるため、テストケースに期待値を記入する必要はありません。テストケースに必要なのは入力値のみです。モデル設計者の方が設計中のちょっとした動作確認に行うような正式なテストに位置付けられないシミュレーションも全てフォーマルテストの対象に加えられます。様々なソースから自動でテストケースを作成することもできます。要求からの自動テストケース生成だけでなく、Back-to-backテストパッケージの機能を用いて構造カバレッジの高いテストケースを自動生成することも可能です。

自動で作成したテストケース、手動で作成したテストケース問わず、シミュレーションした結果は全て判定の対象になります。この要求に対して直接関係の無いつもりで作成したテストケースも、判定の対象になります。一つのテストケースが複数の要求を網羅することもあるかも知れません。テストをしたつもりの要求がテストできていないこともあるかも知れません。それらは全てツールが自動で検出します。同じ質のテストを行うのであれば、記述する量、判定に要する工数、レビューに要する工数、再利用性の観点で、要求の形式化を伴ったとしてもフォーマルテストは従来の手動のテスト手法に比べて十分に有利です。

 

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

フォーマルテストはスケーラブルなテクノロジです。要求の数が非常に多くなる場合には複数台のPCに分けて、または1台のPCでも複数回に分けて実行することが可能です。一台のPCにおける一回の解析でも(用いられるPCの性能、要求の複雑さ、シミュレーション実行記録の規模にもよりますが、)数百の要求を同時に判定対象とすることができます。また、dSPACE社製品から取得したmdf4形式のシミュレーション実行記録であれば、十万ステップ以上のデータも解析できます。もしシミュレーション実行記録データが巨大になり過ぎるほどHILシミュレーションを長時間実行するのであれば、RTT-Observerを用いてHIL実行中にリアルタイムでフォーマルテストの判定を行うことも可能です。(RTT-Observerの場合、同時に監視できる要求の数はHILの性能と実行負荷に応じて、一般には数十に制限されます。)

 

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

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