Abstract
Requirements validation is an essential activity to carry out in the system development life cycle, and it confirms the completeness and consistency of requirements through various levels. Model-based formal methods can provide a cost-effective solution to requirements validation in a wide range of domains such as safety-critical applications. In this paper, we extend a formal language Timed Abstract State Machine (TASM) with two newly defined constructs Event and Observer, and propose a novel requirements validation approach based on the extended TASM. Specifically, our approach can: 1) model both functional and non-functional (e.g. timing and resource consumption) requirements of the system at different levels and, 2) perform requirements validation by utilizing our developed toolset and a model checker. Finally, we demonstrate the applicability of our approach in real world usage through an industrial case study of a Brake-by-Wire system.
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
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R.: Modeling in Event-B - System and Software Engineering. Cambridge University Press (2010)
Bahill, A.T., Henderson, S.J.: Requirements development, verification and validation exhibited in famous failures. Syst. Eng. (2005)
Becker, M., Luckey, M., Becker, S.: Performance analysis of self-adaptive systems for requirements validation at design-time. In: Proceedings of QoSA 2013, pp. 43–52. ACM, New York (2013)
Blom, J., Hessel, A., Jonsson, B., Pettersson, P.: Specifying and generating test cases using observer automata. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 125–139. Springer, Heidelberg (2005)
Börger, E., Stärk, R.F.: Abstract State Machines. A Method for High-Level System Design and Analysis. Springer (2003)
Cardei, I., Fonoage, M., Shankar, R.: Model based requirements specification and validation for component architectures. In: 2008 2nd Annual IEEE Systems Conference, pp. 1–8 (2008)
Cimatti, A., Roveri, M., Susi, A., Tonetta, S.: From informal requirements to property-driven formal validation. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 166–181. Springer, Heidelberg (2009)
Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Comput. Surv. 28(4), 626–643 (1996)
Ellis, A.: Achieving safety in complex control systems. In: Proceedings of SCSC 1995, pp. 1–14. Springer, London (1995)
Iliasov, A.: Augmenting formal development with use case reasoning. In: Brorsson, M., Pinho, L.M. (eds.) Ada-Europe 2012. LNCS, vol. 7308, pp. 133–146. Springer, Heidelberg (2012)
Leveson, N.G.: Safeware: System Safety and Computers. ACM, NY (1995)
Lu, Y.: Pragmatic Approaches for Timing Analysis of Real-Time Embedded Systems. PhD thesis, Mälardalen University (2012)
MAENAD (2013), http://www.maenad.eu
Mashkoor, A., Jacquot, J.-P., Souquières, J.: Transformation Heuristics for Formal Requirements Validation by Animation. In: Proceedings of SafeCert 2009, York, United Kingdom (2009)
OMG (2013), http://www.omgmarte.org/
Ouimet, M.: A formal framework for specification-based embedded real-time system engineering. PhD thesis, Department of Aeronautics and Astronautics. MIT (2008)
Scandurra, P., Arnoldi, A., Yue, T., Dolci, M.: Functional requirements validation by transforming use case models into abstract state machines. In: Proceedings of SAC 2012, pp. 1063–1068. ACM, NY (2012)
Yang, Z., Hu, K., Ma, D., Pi, L.: Towards a formal semantics for the AADL behavior annex. In: Proceedings of DATE 2009, pp. 1166–1171 (2009)
Zhou, J., Johnsen, A., Lundqvist, K.: Formal execution semantics for asynchronous constructs of aadl. In: Proceedings of ACES-MB 2012, pp. 43–48 (2012)
Zowghi, D., Gervasi, V.: The three cs of requirements: Consistency, completeness, and correctness. In: Proceedings of REFSQ 2002 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Zhou, J., Lu, Y., Lundqvist, K. (2014). A TASM-Based Requirements Validation Approach for Safety-Critical Embedded Systems. In: George, L., Vardanega, T. (eds) Reliable Software Technologies – Ada-Europe 2014. Ada-Europe 2014. Lecture Notes in Computer Science, vol 8454. Springer, Cham. https://doi.org/10.1007/978-3-319-08311-7_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-08311-7_5
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08310-0
Online ISBN: 978-3-319-08311-7
eBook Packages: Computer ScienceComputer Science (R0)