Semiformal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints

In recent days, the complexity of software has increased significantly in embedded products in such a way that the verification of embedded software (ESW) now plays an important role to ensure the product´s quality. Embedded systems engineers usually face the problems of verifying properties that have to meet the application´s deadline, access the memory region, handle concurrency, and control the hardware registers. This work proposes a semiformal verification approach that combines dynamic and static verification to stress and cover exhaustively the state space of the system. We perform a case study on embedded software used in the medical devices domain. We conclude that the proposed approach improves the coverage and reduces substantially the verification time.