[Back]

R. Bill, S. Gabmeyer, P. Kaufmann, M. Seidl:
"MocOCL: A Model Checker for CTL-Extended OCL Specifications";
2014; 6 pages.

We present the model checker MocOCL, a tool for model checking software models. The design rationale behind MocOCL is to close the gap between formal verification based on model checking and model-based engineering. Our approach avoids conversions that translate the software models into a format that a model checker can process. To this end, we implemented an explicit state model checker that directly processes the software model and verifies them against a specification formulated in a temporal extension of the constraint language OCL. MocOCL offers a web interface that interacts with the Eclipse Modeling Framework.

We present the model checker MocOCL, a tool for model checking software models. The design rationale behind MocOCL is to close the gap between formal verification based on model checking and model-based engineering. Our approach avoids conversions that translate the software models into a format that a model checker can process. To this end, we implemented an explicit state model checker that directly processes the software model and verifies them against a specification formulated in a temporal extension of the constraint language OCL. MocOCL offers a web interface that interacts with the Eclipse Modeling Framework.

model based engineering, verification, model checking, OCL

http://publik.tuwien.ac.at/files/PubDat_234915.pdf