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

Sammanfattning: 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 resulted in techniques and methods for automated Formal Verification to aid in this endeavour. However, problems still exist with verifying software that is stateful, i.e. where the output of the system depends on its internal state. 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.