ソフトウェア・シンポジウム 2015 in 和歌山 大規模複雑化した組込みシステムための障害診断に おける形式手法の適用事例報告 岡野浩三 信州大学工学部情報工学科 [email protected] 北道淳司 会津大学コンピュータ理工学部 [email protected] 要旨 IPA/SEC ソフトウェア高信頼化推進委員会 障害原因 診断 WG では，大規模・複雑化した組込みシステムで発 生した障害に対する初動調査から障害原因診断分析， 整理に至るまでのプラットフォームとして事後 Verification & Validation(V＆V)を提案している(発表時には参照先を 示す)．本稿では，事後 V&V において，形式手法による 障害原因診断の例を述べる． 1. 図 2 UPPAAL を用いたモデル はじめに 大規模・複雑化した組込みシステムでの障害は社会 への影響が大きく，多くの設計技法や国際規格が提案さ れているがそれでも障害が発生する．本稿では，形式手 法を用いて障害診断を行った例を述べる．形式手法は， 数学的な意味定義が行われた言語および手続きにより システムのモデリングおよびモデルに対する議論(ある性 質が成り立つかどうかなど)が行える．形式手法の一つで あるモデル検査手法を化学プラントに適用し，プラントに 内在する障害を検出し，モデルを修正するまでを述べる (詳細はスライド参照)． 2. 図 3 修正して得られたモデル 一般に，事後 V&V では事故などが発生したあとシス テムの資料などからシステムモデルを作成し，そのモデ ルを解析して事故の原因を究明する．このケーススタ ディでは図１のシステムの要求記述をもとに図 2 のモデ ルを作成した．「水槽はあふれない」ことを時相論理式で 表し，モデル検査を行った結果，性質が成り立たないこ とと反例が示された．反例を解析した結果，モデル（すな わち，当初の制御部の設計）にバグがあることが分かり， それを修正したモデル（設計）を作成し，性質が成り立つ ことを示した． 形式手法を用いた障害診断例 対象は図 1 に示す化学プラントである．2 つの水槽が あり，センサ，操作員による操作を入力として，水槽があ ふれないように制御する．このプラントでは，ある条件に おいて水槽があふれるという障害が発生した．プラントの 制御部に着目し，形式手法の 1 つである UPPAAL[1]を 用いて文献[2]を参考にモデル化した(図 2)． 3. まとめ 組込みシステムの障害に形式手法を適用し，その障害 を検出し，取り除いた事例を述べた．形式手法のこのよう な利用に関する質問，ご意見を伺いたい． [1] Gerd Behrmann, Alexandre David and Kim G. Larsen,” A Tutorial on Uppaal,”LNCS Vol. 3185, pp 200-236, 2004. [2] Kim Björkman, Juho Frits, Janne Valkonen, Jussi Lahtinen, et al., “Verification Of Safety Logic Designs By Model Checking,” Sixth American Nuclear Society International Topical Meeting on Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies, NPIC&HMIT 2009. 図 1対象とした化学プラント 26 SEA
© Copyright 2024 ExpyDoc
