Practical Verification of Stateful Embedded C Code using Finite State Machines and VCC

Mathias Lindgren
mathial@kth.se

Abstract

Vehicles in the 21st-century are becoming more and more dependent on embedded software systems for navigation, system control, monitoring, and entertainment. Manufacturers of cars have also over the years been put under more and more safety regulations and as such, some of these systems are of a safety critical nature and undergo rigorous reliability testing.

Some automotive manufacturers have been investigating the use of Formal Verification as a strategy in ensuring reliability and safety. Previous work has developed techniques and methods for automated Formal Verification to aid in this endeavour. One property of code in embedded systems is statefulness, how the memory of the program changes over time.

To tackle the problems with describing stateful requirements of programs, a model of writing requirements as Finite State Machines is presented. A case study looking at real world requirements on stateful c-code was performed. Verification with previously used tools was successful when writing the requirements in the new style. Future possible improvements and shortcomings are identified.