Presentation 2018-03-06
Model Checking Application to the Railway Crossing Problem for STAMP/STPA using Timed Automaton
Kozo Okano, Shinpei Ogata, Pan Yang, Keishi Okamoto,
PDF Download Page PDF download Page Link
Abstract(in Japanese) (See Japanese page)
Abstract(in English) Recent rapid growth of information systems makes uspay attention to methods for analysis of accident causationand prevention of accidents. One of the new approaches isSTAMP (Systems Theoretic Accident Model and Processes). The approach in STAMP widely analyses causal factorsfrom not only a failure in a component and a human errorbut also interface mismatching among multiple components. STPA (STAMP based Process Analysis) identifies hazardsusing a few guidewords. Hybrid approaches based both STAMP and formal approachesare expected to be promised approaches. From the view point of the above, this report try tomodel the railway crossing problem that is introducedas an example of STAMP analysis process in a network oftimed automata. We also discuss how to combine model checking approachesinto STPA with the results of this case-study.
Keyword(in Japanese) (See Japanese page)
Keyword(in English) STAMP/STPA / Railway Crossing Problem / Timed Automata / Model Checking
Paper # SS2017-64
Date of Issue 2018-02-27 (SS)

Conference Information
Committee SS
Conference Date 2018/3/6(2days)
Place (in Japanese) (See Japanese page)
Place (in English)
Topics (in Japanese) (See Japanese page)
Topics (in English)
Chair Kazuhiro Ogata(JAIST)
Vice Chair Akio Nakata(Hiroshima City Univ.)
Secretary Akio Nakata(Tokyo Inst. of Tech.)
Assistant Kazuyuki Shima(Hiroshima City Univ.)

Paper Information
Registration To Technical Committee on Software Science
Language JPN
Title (in Japanese) (See Japanese page)
Sub Title (in Japanese) (See Japanese page)
Title (in English) Model Checking Application to the Railway Crossing Problem for STAMP/STPA using Timed Automaton
Sub Title (in English)
Keyword(1) STAMP/STPA
Keyword(2) Railway Crossing Problem
Keyword(3) Timed Automata
Keyword(4) Model Checking
1st Author's Name Kozo Okano
1st Author's Affiliation Shinshu University(Shinshu Univ.)
2nd Author's Name Shinpei Ogata
2nd Author's Affiliation Shinshu University(Shinshu Univ.)
3rd Author's Name Pan Yang
3rd Author's Affiliation Shinshu University(Shinshu Univ.)
4th Author's Name Keishi Okamoto
4th Author's Affiliation Sendai National College of Technology(Sendai National College of Tech.)
Date 2018-03-06
Paper # SS2017-64
Volume (vol) vol.117
Number (no) SS-477
Page pp.pp.1-6(SS),
#Pages 6
Date of Issue 2018-02-27 (SS)