Hybrid verificatio of temporal properties in hardware dependent software

The verification of embedded software has become an important subject over the last years. In order to verify temporal properties, formal approaches are efficient, but only applicable for small or medium sized software modules, where they have less state space to explore. Conventional simulation-based methods are still dependent on the systems to be applied and they have additionally the coverage problem, i.e., only the paths executed during the simulation can be monitored. This work presents a semiformal verification approach called SofTPaDS, which is based on the combination of both assertion-based and symbolic simulation approaches for the verification of embedded software with hardware dependencies. This combination shows to be more efficient than the state-of-the-art software model checkers in order to trace deep spaces, and presents improvements of the state coverage relative to a simulation-based verification tool. We have applied our approach to the verification of an industrial automotive embedded software.