Verifying consistency between activity diagrams and their corresponding OCL contracts

Modeling languages such as SysML provide various description means for a precise specification of the desired system. As a system model typically uses multiple diagram types focusing on different aspects, it is crucial to keep them consistent to each other. In this paper, we propose a verification methodology which ensures the consistency between activity diagrams as blueprints for the implementation and their contracts from a block definition diagram. For this purpose, activity diagrams are transformed to OCL constraints that can be checked against pre- and postconditions. The proposed approach is evaluated in a case study based on an industrial specification.