Title: Analyzing UML/OCL Models wit HOL-OCL
Presenters: Achim Brucker and Burkhart Wolff
Duration: half day
When: Monday morning, 20 June 2011
We present the theorem proving environment HOL-OCL. The HOL-OCL system (http://www.brucker.ch/projects/hol-ocl/) is an interactive proof environment for UML/OCL specifications that is integrated in a Model-driven Engineering (MDE) framework. HOL-OCL allows to reason over UML class models annotated with OCL specifications (e.g., class invariants, pre-conditions and post-conditions of methods). Thus, HOL-OCL strengthens a crucial part of the UML to an object-oriented formal method. HOL-OCL provides several derived proof calculi that allow for formal derivations of validity of UML/OCL formulae. These formulae arise naturally when checking the consistency of class models, when formally refining abstract models to more concrete ones or when discharging side-conditions from model-transformations.
In this tutorial, we will explain the foundations of HOL-OCL such as a conservative, shallow embedding of UML/OCL into Isabelle/HOL, and and present several case-studies and applications. For example, we will show how HOL-OCL can be used for analyzing the consistency of UML/OCL specifications.
Achim D. Brucker is a senior researcher and project lead at SAP Research, Germany. His research interests include formal methods, testing, software engineering and security. He has taught and assisted courses at undergraduate and graduate level about distributed programming, theoretical computer science, mathematics, and formal methods. He is a developer of HOL-OCL and participates in the OCL standardization process of the OMG.
Burkhart Wolff is a full professor at at University Paris-Sud, France and member of the Laboratoire de Recherche Informatique (LRI) which is a research institution belonging to the CNRS. He is head of the ForTesSE team. His research interests are focused on Software Verification Environments. This covers top-down refinement methods, bottom-up code verification methods or specification-based testing methods. He has taught and assisted various courses about software engineering, theoretical computer science, and formal methods at undergraduate and graduate level. He is a developer of HOL-OCL.