[Back]

I. Wenzel, R. Kirner, B. Rieder, P. Puschner:
"Cross-Platform Verification Framework for Embedded Systems";
Talk: 5th IFIP Workshop on Software Technologies for Future Embedded & Ubiquitous Systems (SEUS 2007), Santorini, Greece; 2007-05-07 - 2007-05-08; in: "The 5th IFIP Workshop on Software Technologies for Future Embedded & Ubiquitous Systems", (2007), Paper ID p2A-2, 12 pages.

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 crossplatform
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.