Chaining Model Transformations for System Model Verification: Application to Verify Capella Model with Simulink

In the context of Model-Based System Engineering (MBSE), Thales has developed a method called Arcadia, and its dedicated workbench Capella. This approach provides engineer generic practices and tools to design system models in a coherent way. While models grew in complexity, the need emerged for model Simulation and verification. In this paper, a model based approach is proposed to provide an interpretation of the Capella dynamic behavior description of modeled systems. The approach allows targeting different semantics and facilitating reuse of legacy semantics. The idea is to enforce separation of concerns of semantics definition by defining a chain of five transformations. The approach ensures traceability between Capella source models and target models, facilitating interpretation of the verification results. We apply our approach to analyze dataflow diagrams of a Capella "clock radio" model. For this purpose we transform the Capella dataflow model to a Simulink model. The experimentation on the use case demonstrates the ability of the tool to catch model inconsistency problems.