On the integration of model-driven design and dynamic assertion-based verification for embedded software

Model-driven design (MDD) aims at elevating design to a higher level of abstraction than that provided by third-generation programming languages. Concurrently, assertion-based verification (ABV) relies on the definition of temporal assertions to enhance functional verification targeting the correctness of the design execution with respect to the expected behavior. Both MDD and ABV have affirmed as effective methodologies for design and verification of HW components of embedded systems. Nonetheless, MDD and ABV individually suffer some limitations that prevent their integration in the embedded-software (ESW) design and verification flow. In particular, MDD requires the integration of an effective methodology for monitoring specification conformance, and dynamic ABV relies on simulation assumptions, satisfied in the HW domain, but which cannot be straightforward guaranteed during the execution of ESW. In this work, we present a suitable combination of MDD and dynamic ABV as an effective solution for ESW design and verification. A suite composed of two off-the-shelf tools has been developed for supporting this integrated approach. The MDD tool, i.e., radCASE, is a rapid-application-development environment for ESW that provides the user with a comprehensive approach to cover the complete modeling and synthesis process of ESW. The dynamic ABV environment, i.e., radCHECK, integrates computer-aided and template-based assertion definition, automatic checker generation, and effective stimuli generation, making dynamic ABV really practical to check the correctness of the radCASE outcome. (c) 2012 Elsevier Inc. All rights reserved.