文献

J-GLOBAL ID：201802291308030848   整理番号：18A0698388

STAMP/STPA単線列車例題に対する時間オートマトンモデル検査の適用と考察

Model Checking Application to the Railway Crossing Problem for STAMP/STPA using Timed Automaton

著者 (4件)： 岡野浩三 (信州大 工) ,  小形真平 (信州大 工) ,  YANG Pan (信州大 工) ,  岡本圭史 (仙台高専)
資料名： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
巻： 117  号： 477(SS2017 64-77)  ページ： 1-6  発行年： 2018年02月27日 
JST資料番号： S0532B  ISSN： 0913-5685  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 近年情報システムの大規模化複雑化にともない,情報システムの事故原因解明や事故そのものの事前防止策に注目があつまっている。システム理論に基づく事故モデルとして,従来は対応が困難である複雑なシステムに対する分析モデルにSTAMP(Systems Theoretic Accident Model and Processes)がある。STAMPを用いたアプローチでは障害の原因を,コンポーネントの故障や人間のエラーなどに限定せず,コンポーネント間やコンポーネントと人間の間のインターフェイスのミスなどの幅広い視野で分析する。STAMPに基づいた解析手法STPA(STAMP based Process Analysis)では,限定されたガイドワードを用いてハザードの同定を図る。モデルベースの障害診断にSTAMP/STPAの手法を取り入れ,モデル検査や制約指向の仕様検証などの形式手法と組み合わせることにより,より有効な障害診断の枠組みを得ることが期待できる。本稿ではSTAMP解析例題である単線踏切例題に対して動作モデルを時間オートマトンモデルとして構築し,モデル検査機Uppaalで解析したケーススタディについて述べる。また,これをもとにモデル検査技術とSTAMP/STPA手法との連携方法について考察を行う。(著者抄録)

シソーラス用語： *事故分析 ,  プロセス解析 ,  故障診断 ,  *モデル検査 ,  *オートマトン ,  時間依存性 ,  形式的仕様 ,  *踏切 ,  鉄道線路 ,  事例研究 ,  モデリング ,  情報システム ,  システム理論 ,  *ソフトウェア障害 ,  ヒューマンエラー ,  システムインタフェイス
準シソーラス用語： STAMP/STPA ,  時間オートマトン ,  単線踏切

分類 (1件)： 計算機システム開発  (JD02010R)

引用文献 (9件)：

• Nancy Leverson: ′′Engineering a Safer World: Systems Thinking Applied to Safety,′′ MIT Press (2012)
• Sebastian ElbaumS and Rosenblum David: ′′Known unknowns: testing in the presence of uncertainty,′′ Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (2014)
• John Thomas: ′′Extending and Automating a Systems-Theoritic Hazard Analysis for Requirements Generation and Analysis,′′ Ph.D Thesis, Masasachusetts Institute of Technology (2013)
• システム安全性解析WG: ′′はじめてのSTAMP/STPA, 初級編′′, 情報処理推進機構 (2016)
• Johan Bengtsson and Wang Yi: ′′Timed automata: Semantics, algorithms and tools,′′ In Lecture Notes on Concurrency and Petri Nets, volume 3098, pp.87-124 (2004)

タイトルに関連する用語 (5件)： STAMP ,  StpA ,  列車 ,  時間オートマトン ,  モデル検査