[Zurück]


Wissenschaftliche Berichte:

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



Kurzfassung deutsch:
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.

Kurzfassung englisch:
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.

Schlagworte:
model based engineering, verification, model checking, OCL


Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/PubDat_234915.pdf


Erstellt aus der Publikationsdatenbank der Technischen Universitšt Wien.