Art

J-GLOBAL ID：201802291308030848   Reference number：18A0698388

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

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

Author (4)： OKANO KOZO (信州大 工) ,  OGATA SHIMPEI (信州大 工) ,  YANG Pan (信州大 工) ,  OKAMOTO KEISHI (仙台高専)
Material： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
Volume： 117  Issue： 477(SS2017 64-77)  Page： 1-6  Publication year： Feb. 27, 2018 
JST Material Number： S0532B  ISSN： 0913-5685  Document type： Proceedings
Article type： 原著論文  Country of issue： Japan (JPN)  Language： JAPANESE (JA)

Thesaurus term： *accident analysis ,  process analysis (control) ,  fault diagnosis ,  *model checking ,  *automaton ,  time dependence ,  formal specification ,  *railroad crossing ,  railway line ,  case study ,  modeling ,  information system ,  system theory ,  *software failure ,  human error ,  system interface
Semi thesaurus term： STAMP/STPA ,  timed automata ,  単線踏切

JST classification (1)： Computer system development  (JD02010R)

Reference (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)

Terms in the title (5)： STAMP ,  StpA ,  列車 ,  時間オートマトン ,  モデル検査