loader image

モデルベース開発向けのテストソリューション

必数百万ものシナリオをどのようにして作成するか?

テスト数の爆発的増大を避けるには?

テストの合格・不合格をどのように見分けるか?

BTC EmbeddedPlatform

Formal Verification
パッケージ

セーフティクリティカルなソフトウェアに対する要求違反の不在証明

イントロダクション

Formal Verification パッケージ

Formal Verification パッケージはセーフティクリティカルな 要求を形式検証する機能を提供します。

近年の組込み開発プロジェクトにおいて入力信号とキャリブレーションが取り得る値の組合わせは簡単に無限に膨れ上がります。大量のテストケースを作成したとしても、ソフトウェアロジックを通過するすべての経路をカバーすることは困難です。つまり、どんなに厳密なテストを行ったとしても「安全要求に違反しないのか?」という重要な問題は解決されていません。

BTC EmbeddedPlatformはモデルチェック技術により与えられた要求がソフトウェアによって違反されることがないことを自動的に証明します。つまり、入力信号とキャリブレーション値の組み合わせでシステムを安全でない状態に追い込むことは不可能であることを証明します。

サポートされる機能

  • モデルチェックテクノロジによる形式検証 要求違反がないことの数学的な証明を含む 反例の生成を含む
  • MIL/SIL デバッグ環境エクスポート
  • Universal Patternによる形式記述
  • MATLAB API、REST API
Play now
動画再生
Play now
動画再生

FORMAL VERIFICATION パッケージ

ユースケース

形式検証

セーフティクリティカルなシステムに対する要求違反の不在証明

要求の形式化

要求の直感的な形式記述

FORMAL VERIFICATION パッケージ

検証の対象

dSPACE TargetLink

モデルの振舞いの静的解析
Cコードの振舞いの静的解析

Mathworks Embedded Coder

Cコードの振舞いに対する静的解析

Cコード

Cコードの振舞いに対する静的解析

アドオン

RTT-Observer Generator​

RTT-ObserverはBTC Embedded SystemsとdSPACE社の協力で開発されたテクノロジです。このテクノロジはdSPACE VEOSとHILにおけるテストをリアルタイムのフォーマルテストで強化します。

このアドオンは形式化された要求からRTT-Observerと呼ばれる監視ユニットを生成します。各RTT-ObserverはdSPACE HIL/VEOSシミュレーションを監視し、元となった要求が満たされているか否かをリアルタイムでレポートします。

RTT-ObserverとdSPACE HIL/VEOSの並列実行により、テストに要する労力にはほとんど変化なく、各要求に対するテストの深度を劇的に高めることが可能です。さらにControlDesk Next Generation、AutomationDeskを含むdSPACE製品群との高度な統合により、様々なプロジェクトで快適かつ効率的にRTT-Observerを利用することが可能となっています。

備考: このソリューションを利用するためには別途、dSPACE社の製品であるReal Time Testing (RTT) Observer Libraryが必要です。

詳しくはこちらをご覧ください: www.dspace.com

機能安全規格認証

ISO 26262

BTC EmbeddedPlatformがセーフティクリティカルなソフトウェア開発プロジェクトでの利用に適していることは、ドイツTÜV SÜDによって認証されています。 この認証はIEC 61508-3:3010, ISO 26262, EN 50128, IEC 62304, ISO 25119を含む複数の標準規格に言及しています。 自動車用機能安全規格ISO 26262に関しては、ツール信頼レベルの中で最も高いTCL3で認証を受けており、この認証はASIL-Dを含む全てのASILレベルに対して有効です。 認証書と認証レポートは要望に応じてツールユーザ様に無償で提供しています。この認証書はツール認定(Tool Qualification)に要するお客様側の労力を大きく削減致します。

評価用ライセンスの申し込み

私たちの製品を試してみたいと思っていただけたのであれば、喜んで無償の評価用ライセンスを発行致します。御希望であれば評価に無償のツールトレーニングもお付けします。ツールトレーニングは他社と合同ではなく、あなた専用で行います。

セールスエンジニアとのミーティング予約

質問をしてみたかったり、ツールが動いているところを見てみたいという方は下のリンクからミーティングをご予約ください。セールスエンジニアリングチームのメンバーが喜んでご対応致します。

評価用ライセンスの申し込み

私たちの製品を試してみたいと思っていただけたのであれば、喜んで無償の評価用ライセンスを発行致します。御希望であれば評価に無償のツールトレーニングもお付けします。ツールトレーニングは他社と合同ではなく、あなた専用で行います。

セールスエンジニアとのミーティング予約

質問をしてみたかったり、ツールが動いているところを見てみたいという方は下のリンクからミーティングをご予約ください。セールスエンジニアリングチームのメンバーが喜んでご対応致します。

BTC EMBEDDED SYSTEMSのブログ

ブログ

組み込みソフトウェア開発、モデルベースデザイン、自動コード生成、ISO26262準拠のテストに関する情報の公開

製品動画

動画

短い動画で当社製品の主な機能をご覧ください。

Formal Test パッケージ

形式手法により高度に自動化された要求ベーステストと自動テスト生成