Abstract
This work suggests a method for systematically constructing an environment model for automotive operating systems compliant with the OSEK/VDX international standard by introducing a constraint specification language, OSEK_CSL, and defining its underlying formal models. OSEK_CSL is designed for specifying constraints of OSEK/VDX using a pre-defined set of constraint types identified from the OSEK/VDX standard. Each constraint specified in OSEK_CSL is interpreted as a context-free language and is converted into push-down automata using NuSMV, which allows automated test sequence generation using LTL model checking. This approach supports selective applications of constraints and thus is able to control the “degree” of test sequences with respect to test purposes. An application of the suggested approach demonstrates its effectiveness in identifying safety problems.
This work was supported by the National Research Foundation of Korea Grant funded by the Korean Government (NRF-2012R1A1A4A01011788).
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
OSEK/VDX operating system specification 2.2.3
Trampoline – opensource RTOS project, http://trampoline.rts-software.org
Chen, J., Aoki, T.: Conformance testing for OSEK/VDX operating system using model checking. In: 18th Asia-Pacific Software Engineering Conference (2011)
Choi, Y.: Safety analysis of the Trampoline OS using model checking: An experience report. In: Proceedings of 22nd IEEE International Symposium on Software Reliability Engineering (2011)
de la Riva, C., Tuya, J.: Automatic generation of assumptions for modular verification of software specifications. Journal of Systems and Software (2006)
In der Riden, T., Kanpp, S.: An approach to the pervasive formal specification and verification of an automotive system. In: Proceedings of the International Workshop on Formal Methods in Industrial Critical Systems (2005)
Lettnin, D., et al.: Semiformal verification of temporal properties in automotive hardware dependent software. In: Proceedings of Design, Automation, and Test in Europe Conference and Exhibition (April 2009)
Shi, J., et al.: ORIENTAIS: Formal verified OSEK/VDX real-time operating system. In: IEEE 17th International Conference on Engineering of Complex Computer Systems (2012)
Fang, L., et al.: Formal model-based test for AUTOSAR multicore RTOS. In: Proceeding of the IEEE 5th International Conference on Software Testing, Verification and Validation, pp. 251–259 (2012)
Hierons, R.M., et al.: Using formal specifications to support testing. ACM Computing Surveys (2009)
Zhao, Y., et al.: Modeling and verifying the code-level OSEK/VDX operating system with CSP. In: 5th International Symposium on Theoretical Aspects of Software Engineering, pp. 142–149 (2011)
John, D.: OSEK/VDX conformance testing - MODISTARC. In: Proceedings of OSEK/VDX Open Systems in Automotive Networks (1998)
NuSMV: A New Symbolic Model Checking, http://nusmv.irst.itc.it/
Park, M., Byun, T., Choi, Y.: Property-based code slicing for efficient verification of osek/vdx operating systems. In: First International Workshop on Formal Techniques for Safety-Critical Systems (2012)
Tkachuk, O., Dwyer, M.B., Pasareanu, C.S.: Automated environment generation for software model checking. In: 18th IEEE International Conference on Automated Software Engineering, pp. 116–129 (October 2003)
Yatake, K., Aoki, T.: Automatic generation of model checking scripts based on environment modeling. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol. 6349, pp. 58–75. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Choi, Y. (2013). Constraint Specification and Test Generation for OSEK/VDX-Based Operating Systems. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds) Software Engineering and Formal Methods. SEFM 2013. Lecture Notes in Computer Science, vol 8137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40561-7_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-40561-7_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40560-0
Online ISBN: 978-3-642-40561-7
eBook Packages: Computer ScienceComputer Science (R0)