論文

査読有り
2017年

Automating time series safety analysis for automotive control systems in STPA using weighted partial Max-SMT

Communications in Computer and Information Science
  • Shuichi Sato
  • ,
  • Shogo Hattori
  • ,
  • Hiroyuki Seki
  • ,
  • Yutaka Inamori
  • ,
  • Shoji Yuen

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.

リンク情報
DOI
https://doi.org/10.1007/978-3-319-53946-1_3
ID情報
  • DOI : 10.1007/978-3-319-53946-1_3
  • ISSN : 1865-0929
  • SCOPUS ID : 85013249214

エクスポート
BibTeX RIS