ソリューション

形式検証ソリューション

車載システムや基幹システム等、不具合の発生が絶対に許されないソフトウェアにおいては品質・安全性を最大限まで追求する必要があり、機能安全規格では形式検証による品質保証が推奨されています。
当社はモデル検査をはじめとする形式検証手法を利用してお客様の課題解決をお手伝いします。

関連キーワード

Event-B,SPIN,モデル検査,仕様の矛盾・抜け漏れ,信頼性,安全性,定理証明,形式仕様記述,形式手法,形式検証,機能安全,状態遷移モデル

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

ソリューション概要

サービス内容

形式検証の導入・運用支援コンサルティング

  • 形式検証の初期導入支援
  • 形式検証の運用支援

形式検証に必要なツール環境の提供・カスタマイズ

  • STATURE+テンプレートの提供(自然言語による要求仕様定義)
  • UMLツール+アドインの提供(モデリング環境、形式検証コード生成、結果の可視化)
  • 各種ツールの新規作成、カスタマイズ

形式検証の請負サービス

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

適用対象分野

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

  • 高い安全性が要求される交通システム
    例)自動車車載システム、鉄道制御システム
  • 莫大な投資を要する航空宇宙システム
    例)航空管制システム、人工衛星制御システム
  • 不具合による社会的影響度が甚大な社会インフラ・基幹システム
    例)原子力発電所制御システム、銀行情報システム

このソリューションで解決できること

【形式検証(定理証明)による要求仕様の矛盾、抜け漏れの検出】

  • 要求をSTATUREテンプレート(*)上で自然言語に近い形の形式仕様記述で表現します。
  • 要求仕様を形式検証モデルに自動変換し、形式検証/定理証明(**)で要求の矛盾、抜け漏れを検出し、要求仕様が正しいことを証明します。

【形式検証(モデル検査)による振る舞いの欠陥の検出】

  • 要求仕様に従いUML等のモデリングツール(***)で振る舞いをモデル化/詳細化します。
  • 振る舞いモデルを形式検証モデルに自動変換し、形式検証/モデル検査(****)で起こり得る状態遷移を網羅検査し、不具合状態に陥る可能性がある(ない)ことを証明します。

【UMLツール環境による利便性の向上】

形式検証言語/ツール仕様等の専門知識を必要とせず、UMLツール上で形式検証による品質向上を実現します。

  • UMLモデル(ステートマシン図、アクティビティ図等)からモデル検査言語コードへ自動変換
  • モデル検査実行結果(反例:不具合に至るまでの状態遷移過程)をUMLツール上でアニメーション表示、EXCEL上で可視化

*「STATURE」は、グローバルに要求される国際規格や法令に沿ったリスクマネジメントに多数の実績を持つ、品質・リスクライフサイクルマネジメントソリューションです。

詳細:http://solution.kke.co.jp/sphera/solutions/iso26262.html

** 定理証明ツールとしては「Event-B&Rodin」をご提案しています。

*** モデリングツールとしては、スパークスシステムズジャパン社が提供する「Enterprise Architect」をご提案しています。

**** モデル検査ツールとしては「SPIN」をご提案しています。

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

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