Asserting Functional Equivalence between C Code and SCADE Models in Code-to-Model Transformations
Resumo
Model-based development is on the rise and tool chains employing automated code generation from models using certified code generators are getting increasingly common. We present an approach which enables the reverse operation and creates an ANSYS SCADE model that is functionally equivalent to the C code. The main motivation behind this development is to enable original equipment manufacturers (OEMs) to further use and maintain legacy code in new development environments, rather than having to re-develop the respective functionality from scratch.While the model transformation itself is performed manually, the testing process is fully automated and enabled the transfer of existing test cases for the C function to the SCADE Test Environment. The presented approach enables white-box testing of the model, requiring the original C implementation and its original test cases as well as a bi-directional mapping of variable names between C code and SCADE model. This is done by extending the original code in a way that generates SCADE test scenarios during runtime, allowing to use these white-box test scenarios to assert functional equivalence of code and model using empirical validation.