• BPnet
  • ビジネス
  • IT
  • テクノロジー
  • 医療
  • 建設・不動産
  • TRENDY
  • WOMAN
  • ショッピング
  • 転職
  • ナショジオ
  • 日経電子版

HOMEエレクトロニクス電子設計組み込み業界では今、何が起きているのか > モデル検証技術の活用

  • 岡野 浩三(信州大学 准教授、IPA/SEC システム安全性・信頼性分析手法WG委員)、岡本 圭史(仙台高等専門学校准教授、IPA/SEC システム安全性・信頼性分析手法WG委員)
  • 2016/11/16 00:00
  • 1/6ページ

 近年、これまで個別に動作していたシステムがさまざまなレベルのネットワークを通じて相互に結ばれて協調動作するようになっている。このように複雑化したシステムに対する安全分析や障害原因診断では、推定要因とその箇所を絞り込んだ後に、絞り込んだ推定要因が本当の要因であることを検証することになる。また、システムの複雑化への対応策として、モデルベースでこうした分析・診断を行うようになってきている。

 例えば、システムのコンポーネント間の相互作用に着目した安全分析手法である「STAMP(System Theoretic Accident Model and Processes)/STPA(System Theoretic Process Analysis)」を用いて分析することにより、システム全体の障害を引き起こす推定要因を「コンポーネントCが性質Pを満たさないこと」といったように絞り込めることがある。推定された要因に対するモデルベース検証技術の1つが「形式手法」である。本稿では、形式手法について解説する。まず代表的な形式検証である「モデル検査」を解説し、続いて形式手法のバックエンドとして注目を浴びている「SAT(boolean SATisfiability)/SMT(Satisfaction Modulo Theory)ソルバ」を解説する。

おすすめ