Enabling dynamic assertion-based verification of embedded software through model-driven design

Assertion-based verification (ABV) is more and more used for verification of embedded systems concerning both HW and SW parts. However, ABV methodologies and tools do not apply to HW and SW components in the same way: for HW components, both static ABV and dynamic ABV are widely used; on the contrary, SW components are traditionally verified by means of static ABV, because dynamic approaches are based on simulation assumptions which could not be true during execution of general embedded SW and which cannot be controlled by the assertion language. This paper proposes to exploit model-driven design for guaranteeing such simulation assumptions. Then, it describes an ABV framework for embedded SW, that automatically synthesizes assertion checkers to verify the embedded SW accordingly to the simulation assumptions.