The verification of the system behavior is essential during the early phases of the development of embedded, safety-critical systems. Such systems usually interact with their environment during their operation by controlling actuators based on observations and measurements of sensors. The design-time verification often includes the simulation of the environment by providing data to sensors based on the output of actuators and predefined environmental information, while also monitoring the internal state and behavior of the system.
Matlab-Simulink is a modeling and simulation tool that is popular and wide-spread in the development of embedded, safety-critical systems. Simulink supports the hierarchical implementation of complex systems and the simulation of the system components. Unfortunately, due to the generic modeling approach of Simulink, it is difficult to validate that the components in the prepared model conform to the structural constraints defined for the designed system. These constraints often describe graph-based restrictions on the architecture of the developed system which are hard to specify with a clear, imperative definition.
We have developed an approach for the validation of system constraints on Simulink models, where constraints are defined declaratively and arbitrary Simulink models can be checked for violations. Our solution offers two separate ways to carry out the validation of a model.
One of the methods first transforms Simulink models to the model representation of the Eclipse Modeling Framework then the validation is performed using the EMF-IncQuery model query engine. Based on the incremental evaluation techniques and the EMF model representation provided by the EMF-IncQuery, the approach can scale up to Simulink models with hundreds of thousands of elements. Our technique can automatically annotate the results provided by the model query engine back to the Simulink models, thus the corresponding, constraint-violating parts of the model can be properly identified.
The other offered method generates imperative Matlab validation functions using the declarative description of model constraints. For code generation, the steps of local-search based techniques are applied, instead of an incremental approach used by the other introduced validation method. In this case only the constraint definition is done outside the Matlab environment, all other steps of the process are carried out directly using models in Simulink.