2017年
Automating time series safety analysis for automotive control systems in STPA using weighted partial Max-SMT
Communications in Computer and Information Science
- ,
- ,
- ,
- ,
- 巻
- 694
- 号
- 開始ページ
- 39
- 終了ページ
- 54
- 記述言語
- 英語
- 掲載種別
- 研究論文(国際会議プロシーディングス)
- DOI
- 10.1007/978-3-319-53946-1_3
- 出版者・発行元
- Springer Verlag
Recently, Systems-Theoretic Process Analysis (STPA) has been studied for automobile safety analysis. When STPA is used later in the design phase, significant effort is required to detect causal scenarios of unsafe control actions (UCAs), especially those related to intermittent disturbances in multiple signals. We propose a method to automate this disturbance detection by checking the satisfiability of trace formulas extended with cushion variables. At a state transition, cushion variable values are used instead of original variable values to determine the next state. A signal disturbance is regarded as assigning different values to variables and corresponding cushion variables. Specifying the equality between variables and cushion variables as soft clauses, a Weighted Partial Max-SMT solver mechanically searches an assignment for a trace to satisfy the UCA property. We applied the proposed technique to a simplified automotive control system to demonstrate some examples of automatic detections of reasonable intermittent multi-signal disturbances.
- ID情報
-
- DOI : 10.1007/978-3-319-53946-1_3
- ISSN : 1865-0929
- SCOPUS ID : 85013249214