Abstract
Safety-relevant software developed within the automotive domain is subject to the safety standard ISO 26262. In particular, a supplier must show that implemented safety mechanisms sufficiently address relevant failure modes. This involves complex and costly testing procedures.
We introduce an early analysis approach for safety mechanisms implemented in safety-relevant software by combining model checking and model-based testing. Model checking is applied to verify the correctness of an abstract amodel of the system under test. The verified model is then used to automatically generate tests for the verification of the implemented Safety Elements. The approach has been evaluated in an industrial case study, addressing Analogue Digital Converters as part of the motor control within a hybrid electric vehicle. The results suggest that our approach allows to create high quality test suites. In addition, the test model helps to reduce misunderstandings due to imprecise specification of safety mechanisms.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Here, \(\leadsto \) is the response operator. \(\varphi \leadsto \psi \) for UPPAAL-TCTL formulae \(\varphi \) and \(\psi \) means: whenever \(\varphi \) is fulfilled at a certain moment in time, \(\psi \) must be true at a later point in time. This is the UPPAAL-equivalent of the CTL formula \(\mathbf{AG (\varphi \rightarrow \mathbf AF \psi )}\).
References
ISO/DIS 26262–1 - Road vehicles Functional safety Part 1 Glossary. Technical report, Geneva, Switzerland, July 2009
Specification of ADC Driver. Technical report (2011). http://www.autosar.org/fileadmin/files/releases/4-0/software-architecture/peripherals/standard/AUTOSAR_SWS_ADCDriver.pdf
VeTeSS - Verification and Testing to support functional Safety Standards (2012). http://vetess.eu/
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL 4.0 (2006). http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf
Braspenning, N., van de Mortel-Fronczak, J.M., Rooda, J.E.: A model-based integration and testing method to reduce system development effort. Electron. Notes Theor. Comput. Sci. 164(4), 13–28 (2006)
Bruns, G., Sutherland, I.: Model checking and fault tolerance. In: Johnson, M. (ed.) AMAST 1997. LNCS, vol. 1349, pp. 45–59. Springer, Heidelberg (1997)
Hänsel, J., Rose, D., Herber, P., Glesner, S.: An evolutionary algorithm for the generation of timed test traces for embedded real-time systems. In: 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation (ICST), pp. 170–179, March 2011
Hazelhurst, S., Arlat, J.: Specifying and verifying fault tolerant hardware. In: Proceedings of the Designing Correct Circuits (2002)
Hessel, A.: Model-based test case generation for real-time systems. Acta Universitatis Upsaliensis (2007)
Hessel, A., Pettersson, P.: COVER - a real-time test case generation tool. In: 19th IFIP International Conference on Testing of Communicating Systems (2007)
Joshi, A., Miller, S.P., Whalen, M., Heimdahl, M.P.: A proposal for model-based safety analysis. In: Digital Avionics Systems, vol. 2, pp. 13-pp. IEEE (2005)
Acknowledgement
This work was funded by the German Federal Ministry of Education and Research and the European Union in the context of the European VeTeSS project [3] (ARTEMIS Joint Undertaking, Grant No. 295311).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Gulan, S., Harnisch, J., Johr, S., Kretschmer, R., Rieger, S., Zalman, R. (2015). Model-Based Analysis for Safety Critical Software. In: Koornneef, F., van Gulijk, C. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2014. Lecture Notes in Computer Science(), vol 9337. Springer, Cham. https://doi.org/10.1007/978-3-319-24255-2_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-24255-2_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24254-5
Online ISBN: 978-3-319-24255-2
eBook Packages: Computer ScienceComputer Science (R0)