ソリューション

形式検証ソリューション

どんなにテストをしても検出できない不具合はありませんか?上流設計の検証は熟練レビュアに依存していませんか?昨今、様々業界でフロントローディングによる上流工程での品質・安全性の作りこみが求められています。KKEでは「形式検証」と呼ばれる手法を用いて、お客様の上流設計における課題を解決します。

関連キーワード

形式手法、形式検証、モデル検査、SPIN、機能安全、信頼性、安全性、仕様の矛盾・抜け漏れ、状態遷移モデル、UML、SysML、MBSE

WEBサイト別ウインドウが開きます PDFカタログ別ウインドウが開きます

ソリューション概要

「形式検証」はソフトウェアの複雑な制御設計を検証するのに非常に有用な手法です。形式検証を導入することで、開発上流工程における制御設計において、異常系の動作シナリオ等の人間では見落としがちな振る舞いを早期に発見し、不完全な仕様や設計を作り込むことを防ぐことができます。

熟練者に依存しない検証

  • 上流工程における設計は、複雑であればあるほど熟練者の経験知をベースにレビューされがちですが、熟練者が退職、または異動してしまうと、十分な検証ができなくなってしまう恐れがあります。
  • 形式検証を導入することで、システマティックな検証が可能となり、レビューの属人化を軽減することができます。

人間系では発見困難な不具合の検出

  • 「どれだけレビューやテストを重ねても不具合がなくならない」ということは、設計者の悩みの種であると思います。
  • KKEでは形式検証の手法のひとつである「モデル検査」を用いて、設計対象の「網羅検査」を実施します。これにより、人間系では発見が困難な不具合も検出することが可能です。

手戻りの軽減

  • テスト工程で発見される不具合のうち、その多くが上流に起因すると言われています。
  • 不具合が上流に起因していた場合、上流まで遡って設計を修正する必要があり、膨大な手戻りコストが発生する可能性があります。
  • KKEの形式検証ソリューションでは、上流工程で早期に不具合を検出することにより、手戻りを軽減することが出来ます。

形式検証に関する専門知識は不要

  • 形式検証の実施には専用言語や理論の習得は必要ですが、多忙な現場担当者がこれらを習得することは現実的には困難です。
  • KKEでは設計者が専門的な技術や知識を習得せずとも、形式検証の実施を可能にするツール(※)を提供しています。
  • ツールの導入時には、ツール使用を前提としたUMLの基本的な書き方やツールの使用方法についてトレーニングも実施します。

(※)スパークスシステムズ ジャパンが提供する「Enterprise Architect」で記述したUMLモデルが要求を満たしているかの厳密な検証(形式検証:モデル検査)を支援します。

弊社の形式検証サービス

弊社は以下の形式検証サービスを提供致します。

①形式検証に必要なツール環境の提供・カスタマイズ、及び、形式検証の導入・運用支援コンサルティング

■UMLツール+アドインの提供(モデリング環境、形式検証コード生成、結果の可視化)

■各種ツールの新規作成、カスタマイズ

■モデル化のノウハウや、ツールの使用方法に関するトレーニング

■その他、必要に応じてシステム開発も実施します。

②形式検証の請負サービス

■個別案件の形式検証の請負実施

形式検証の適用対象分野

機能安全規格(ISO 61508/26262等)では高い安全度水準(SIL)が求められるシステムには形式検証の適用が推奨されています。

■高い安全性が要求される交通システム

【弊社実績】ハイブリッド車の走行モード制御、EVのシステム起動/停止制御(自動車OEM様)

【弊社実績】踏切制御システム(JR東日本様)

■莫大な投資を要する航空宇宙システム

【弊社実績】冗長センサシステムによる飛翔体の位置推定ロジックの検証 (JAXA様、SED様)

■不具合による社会的影響度が甚大な社会インフラ・基幹システム

  • 原子力発電所制御システム、銀行情報システム・・・

ソリューションに関するお問い合せ

事業開発部 AOR研究室
TEL:03-5342-1065
E-Mail:aor-bizdev@kke.co.jp