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 im-portant role to ensure the product’s quality. Embedded sys-tems engineers usually face the problems of verifying prop-erties that have to meet the application’s deadline, access the memory region, handle concurrency, and control the hardware registers. This work proposes a semiformal ver-ification approach that combines dynamic and static veri-fication 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 sub-stantially the verification time.