Motivating Model Checking of Embedded Systems Software

The design paradigm shift observed in nowadays embedded software engineering from low level assembly code to high level languages enables ever more advanced applications. With the unprecedented level of actual design and implementation complexity, traditional concepts such as software testing and debugging are reaching their limits of useful application for the verification of ultra-high reliable embedded software. This paper addresses the problems that arise when using C-code for embedded targets and emphasizes the need of detailed knowledge of the underlying hardware architectures. Furthermore, model checking of assembly code is motivated and utilized to find errors in the code that are not obvious at the C-code level and will only occur on very rare occasions in the field. For that purpose we make use of the model checker [mc]square, developed by the RWTH Aachen University, and show some concepts to overcome the traditional model checking showstopper - the state-explosion problem.