Formal Specificationパッケージ

Formal Specificationパッケージは要求の準形式化に必要な機能に絞ったエディタツールです。

Formal Specification パッケージ

BTC EmbeddedPlatformのFormal Specificationパッケージは、Universal Patternを用いた要求の準形式化をサポートしています。準形式化された要求は、モデルチェックによる形式検証、フォーマルテスト、要求のCCC分析に利用できます。このパッケージはFormal Test BASEパッケージ、Formal Testパッケージ、Formal Verificationパッケージ、Requirements Analysisパッケージ共通で利用されているUniversal Patternによる要求の形式化エディタのみをサポートしています。各種モデルやコードのインポート、及び検証機能は含まれません。 

Formal Specificationパッケージ

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

*1 モデルやコードとのマッピング機能は含まれません。モデルやコードとのマッピングには、Formal Test BASEパッケージ、Formal Testパッケージ、またはFormal Verificationパッケージが必要となります。

追加可能なアドオン

 

要求の形式化

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

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

 

各種機能安全規格準拠 

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

 

要求を形式化するメリットは?

要求を形式化することで、コンピュータに要求を理解させ、各種検証・テストの高度な自動化を行えます。これにより手動では不可能な量のテストを実施することや、定量的なテスト品質の管理が可能になります。詳細はテスト・検証の高度な自動化及び要求記述と形式化をご覧ください。