Model-Driven Design and Validation of Embedded Software

This paper presents a model-based framework for designing and validating embedded software (ESW). The design infrastructure is a rapid-application-development suite for ESW, i.e., radCASE, which provides the user with an off the shelf designing environment based on model-driven paradigm. The validation infrastructure, i.e., radCHECK, is based on Property Editor. Such an editor simplifies the definition of PSL properties by exploiting PSL-based templates, that can be automatically compiled into executable checkers by using the integrated Checker Generator engine. Besides, rad-CHECK comprises a testcase generation infrastructure, i.e., Ulisse, which is based on an corner-case oriented concolic approach for ESW, thus it is able to simulate the ESW and the checkers by using high-coverage testcases.