Semiformal verification of temporal properties in automotive hardware dependent software

The verification of embedded software has become an important subject over the last years. This work presents a new semiformal verification approach called SofTPaDS. It combines assertion-based and symbolic simulation approaches for the verification of embedded software with hardware dependencies. SofTPaDS shows to be more efficient than the software model checkers in order to trace deep state spaces and improves the state coverage relative to a simulation-based verification tool. We have successfully applied our approach to an industrial automotive embedded software.