Talks and Poster Presentations (with Proceedings-Entry):
T. Reinbacher, A. Steininger, T. Müller, M. Horauer, J. Brauer, S. Kowalewski:
"Hardware support for efficient testing of embedded software";
Talk: The 7th ASME/IEEE International Conference on Mechatronic and Embedded Systems and Applications,
- 2011-08-31; in: "International Conference on Mechatronic and Embedded Systems and Applications",
Verification of software for embedded systems is crucial for ensuring a product's integrity. Formal approaches like static analysis and model checking are gaining momentum in this context. To make an exhaustive examination of the system's state space tractable in practice, these methods perform an abstraction and over-approximation of the possible behavior. As a side-effect, however, this leads to ``false negatives" -- property violations that exist only in the model and not on the real system. Ruling out such spurious property violations by manual valuation is a tedious and error-prone process. This paper reports on the concepts and design of a hardware unit to support the identification of false negatives. Our approach has several advantages: (i) It works on microcontroller binary code, thus avoiding the need for availability of high-level source code, and covering compiler bugs as well. (ii) Moving the verification directly to the target platform rules out modeling errors. (iii) The cases suspected to lead to spurious property violations can serve as very efficient test cases for a specific implementation later on. We illustrate principle and benefits of the proposed approach by a worked example.
Project Head Andreas Steininger:
Framework für CounterExample Validierung und Testfallgenerierung für die Verifikation von eingebetteter Software
Created from the Publication Database of the Vienna University of Technology.