Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
It is a design decision whether a certain mechanism is introduced in the system to protect a critical signal (\( VehicleSpeed \), in this example) from disturbance, though protecting all signals against disturbance is unrealistic.
References
Leveson, N.G.: Engineering a Safer World: Systems Thinking Applied to Safety. MIT Press, Cambridge (2011)
Leveson, N.G.: A systems-theoretic approach to safety in software intensive systems. IEEE Trans. Dependable Secure Comput. 1, 66–86 (2004)
Sotomayor, R.: Comparing STPA and FMEA on an automotive electric power steering system. In: STAMP Workshop, Boston (2015)
Balgos, Y.: A systems theoretic application to design for the safety of medical diagnostic devices. Master Dissertation, Boston (2012)
Ericson, C.: Fault tree analysis - a history. In: Proceedings of the International System Safety Conference (1999)
Procedure for Performing a Failure Mode Effect and Criticality Analysis. In: United States Military Procedure, MIL-P-1629 (1949)
Troyan, J.E., Vine, L.Y.L.: HAZOP. Loss Prev. 2, 125 (1968)
Owens, B., Herring, M., Dulac, N., Leveson, N., Ingham, M., Weiss, K.: Application of a safety-driven design methodology to an outer planet exploration mission. In: IEEE Aerospace Conference, pp. 1–24. Big Sky, USA (2008)
Dong, A.: Applicaton of CAST and STPA to railroad safety in China. Master’s thesis, Massachusetts Institute of Technology (2012)
Thomas, J., Ang, Y.H., Chung, K., Gao, O.Q.: STPA analysis of intravenous patient-controlled analgesia. In: STAMP Workshop (2016)
Hommes, Q.V.E.: Safety analysis approaches for automotive electronic control systems. In: Society of Automotive Engineers’ Meeting (2015)
Abdulkhaleq, A., Wagner, S.: Experiences with applying STPA to software-intensive systems in the automotive domain. In: STAMP Workshop, Boston (2013). http://www.iste.unistuttgart.de/fileadmin/user_upload/iste/se/publ/Application_of_STPA_to_Automative_Domain.pdf
Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. ACM SIGPLAN Not. 46(6), 437–446 (2011)
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24730-2_15
Dutertre, B., Moura, L.D.: The YICES SMT solver. http://yices.csl.sri.com/
Thomas, J., Suo, D.: STPA-based method to identify and control feature interactions in large complex systems. In: Proceedings of the 3rd European STAMP, Amsterdam (2015)
Lamraoui, S.-M., Nakajima, S.: A formula-based approach for automatic fault localization of imperative programs. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 251–266. Springer, Heidelberg (2014). doi:10.1007/978-3-319-11737-9_17
Hattori, S., Yuen, S., Seki, H., Sato, S.: Automated hazard analysis with pMAX-SMT for automobile systems. In: Pre-proceedings of the International Workshop on Automated Verification of Critical Systems, Edinburgh (2015)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Sato, S., Hattori, S., Seki, H., Inamori, Y., Yuen, S. (2017). Automating Time Series Safety Analysis for Automotive Control Systems in STPA Using Weighted Partial Max-SMT. In: Artho, C., Ölveczky, P. (eds) Formal Techniques for Safety-Critical Systems. FTSCS 2016. Communications in Computer and Information Science, vol 694. Springer, Cham. https://doi.org/10.1007/978-3-319-53946-1_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-53946-1_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-53945-4
Online ISBN: 978-3-319-53946-1
eBook Packages: Computer ScienceComputer Science (R0)