THE FUTURE IS NOW

JAMSSの統合フォーマル検証 IV&V OF JAMSS

JAMSSの統合フォーマル検証とは

JAMSSは、大学研究室との共同研究を重ね、モデル検査を大規模なシステムに適用するための技術を開発してきました。その成果が、「統合フォーマル検証」です。厳密な検証を可能とするフォーマル検証を、システムの全ての機能に適用することは膨大な解析となり事実上不可能です。「統合フォーマル検証」では、ハザード発生要因のみにフォーマル検証の範囲を絞り込み、現実的な工数で網羅的な分析を実現します。

JAMSSの「統合フォーマル検証」は、すでに10年以上の実績を誇ります。ハザード解析手法には、世界中であらゆる技術分野に適用されているSTAMP、レジリエンス・エンジニアリングを採用。フォーマル検証も分野を問わず世界中で研究されてきた手法です。この普遍的な技術に加え、JAMSS独自の解析ツールの併用により、現在、宇宙の他、自動車、航空、鉄道、原子力で大きな成果をあげています。

ハザード解析
STAMP、レジリエンス・エンジニアリングなどの手法を用いて、どのようなときに安全が脅かされるのかを初期段階の仕様から網羅的に解析し、検証が必要な箇所を絞り込みます。絞り込まれた箇所については、理論上起こりうる全ての条件について徹底的にフォーマル検証を行います。

フォーマル検証
数学モデル上でシステムのあらゆる動作パターンを検査し、意図した結果を生むことを証明する手法です。厳密な証明が可能ですが、モデル構築のコストや、検査にかかる時間が膨大になるという課題があります。JAMSSでは、ハザード解析により、検査範囲を絞り込むことで、この問題を克服しています。

JAMSSの統合フォーマル検証とは

JAMSSの統合フォーマル検証のメリット

JAMSSの統合フォーマル検証のメリット

JAMSSの統合フォーマル検証のメリット

JAMSSの統合フォーマル検証は、現実的な工数で網羅的な分析を実現します。

1. 独立した視点
独立した視点から開発者が見逃した問題点を検出

2. コスト削減
検証箇所を絞り込み、不要な試験を避けるので、人的・時間的・費用的コストを削減できる。

3. 全ての危険性を検証
危険可能性がある箇所は全ての条件の組み合わせを検査するため「想定外」を残さない。