Abstract
Many innovations in the automotive sector involve complex electronics and embedded software systems. Testing techniques are one of the key methodologies for detecting faults in such embedded systems.
In this paper, a novel cross-platform verification framework including automated test-case generation by model checking is introduced. Comparing the execution behavior of a program instance running on a certain platform to the execution behavior of the same program running on a different platform we denote cross-platform verification. The framework supports various types of coverage criteria. It turned out that end-to-end testing is of high importance due to defects occurring on the actual target platform for the first time.
Additionally, formal verification can be applied for checking requirements resulting from the specification using the same model generation mechanism that is used for test data generation. Due to a novel self-assessment mechanism, the confidence into the formal models is increased significantly.
We provide a case study for the Motorola embedded controller HCS12 that is heavily used by the automotive industry. We perform structural tests on industrial code patterns using a wide-spread industrial compiler. Using our technique, we found two severe compiler defects that have been corrected in subsequent releases.
This work has been partially supported by the FIT-IT research project “Systematic test case generation for safety-critical distributed embedded real time systems with different SIL levels (TeDES)” and the FWF research project “Compiler-Support for Timing Analysis” (CoSTA).
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
Laprie, J.C., Randell, B.: Basic concepts and taxonomy of dependable and secure computing. IEEE Trans. Dependable Secur. Comput. (Fellow-Algirdas Avizienis and Senior Member-Carl Landwehr) 1(1), 11–33 (2004)
Lackner, K.: Bordelektronik im Zwielicht Economy Austria - Printausgabe (25 August 2006)
Commission, I.E.: Functional safety of electrical / electronic / programmable electronic safety-related systems. IEC standard 61508 (1998)
Software considerations in airborne systems and equipment certification. RTCA/DO-178B (1992)
Beyer, D., Chlipala, A.J., Henzinger, T., Jhala, R., Majumdar, R.: Generating tests from counterexamples. In: Proc. 26th International Conference on Software Engineering (ICSE), Edinburgh, pp. 326–335. IEEE Computer Society Press, Los Alamitos (2004)
Rayadurgam, S., Heimdahl, M.P.E.: Coverage based test-case generation using model checkers. In: Proc. 8th IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2001), IEEE Computer Society Press, Washington, DC (2001)
Ammann, P., Black, P.E., Majurski, W.: Using model checking to generate tests from specifications. In: Proc. 2nd IEEE International Conference on Formal Engineering Methods, Brisbane, pp. 46–54. IEEE Computer Society Press, Los Alamitos (1998)
Hamon, G., deMoura, L., Rushby, J.: Generating efficient test sets with a model checker. In: 2nd International Conference on Software Engineering and Formal Methods, pp. 261–270. IEEE Computer Society Press, Los Alamitos (2004)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Koenig, A.: C Traps and Pitfalls. Addison-Wesley, Reading (1988)
Wenzel, I.: Measurement-Based Timing Analysis of Superscalar Processors. PhD thesis, Technische Universität Wien, Institut für Technische Informatik, Treitlstr. 3/3/182-1, 1040 Vienna, Austria (2006)
Wenzel, I., Rieder, B., Kirner, R., Puschner, P.: Automatic timing model generation by CFG partitioning and model checking. In: Design, Automation and Test in Europe, 2005. Proceedings, pp. 606–611 (2005)
Clarke, E., Kroening, D.: Hardware verification using ANSI-C programs as a reference. In: Proceedings of ASP-DAC 2003, pp. 308–311. IEEE Computer Society Press, Los Alamitos (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 IFIP International Federation for Information Processing
About this paper
Cite this paper
Wenzel, I., Kirner, R., Rieder, B., Puschner, P. (2007). Cross-Platform Verification Framework for Embedded Systems. In: Obermaisser, R., Nah, Y., Puschner, P., Rammig, F.J. (eds) Software Technologies for Embedded and Ubiquitous Systems. SEUS 2007. Lecture Notes in Computer Science, vol 4761. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75664-4_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-75664-4_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75663-7
Online ISBN: 978-3-540-75664-4
eBook Packages: Computer ScienceComputer Science (R0)