Validation of System-level Properties at Code Level

This chapter claims that code generation can be adapted to enable the expression of system-level properties at code level, and be later proved with respect to the code semantics. All previous analyses were performed on discrete dynamical systems models. However, once the control-level properties have been expressed and analyzed at model level, their validity must be asserted on the code artifact extracted from the model. Luckily, this extraction of code from models is largely automatized thanks to autocoding framework generating embedded code from dataflow models. Indeed, code generation from dataflow language is now effective and widely used in the industry. With these in mind, the chapter first gives an overview of the modeling framework, enabling the expression of properties at model and code level. A second part explains the generation of such code annotations, while a last part focuses on their verification.