The expressive power of Z in Object Oriented Modeling, MDE, MDA

Modeling in Z

When designing complex object models, and the expressive power of relational languages is needed in complement to class diagrams.

Formal Specification of Constrained Object Models

Zoomdea aims at sharing Z based Latex resources. This is currently mainly useful for researchers, since it allows for formally specifying constrained object models. Such a formal specification may then be automatically exploited by type checkers like Fuzz, or theorem provers like Isabelle HOL Z, or other tools as Community Z Tools.

Constrained Object Models

Constrained Object Models occur in many areas in industry or research. Normally, UML Class Diagram graphics do not suffice in representing the exact instance set of an object model. More constraints must be specified to filter out unwanted solutions, which requires stating constraints in e.g. the Object Constraint Language (OCL). However, OCL suffers from many expressive deficiencies, or at least, the statement of some constraints can be difficult or cumbersome.

UMZ Applications

We use Z to overcome some of the modeling difficulties raised by OCL. As such we deal only about modeling and do not provide tool support belong the existing. Aplications for the joined modeling power of UML (for the diagrams) + Z (for the semantics) arise for instance in :

UMZ in its current form is extremely simple and flexible. Interestingly enough, the choice of Object Oriented semantics is unlimited, and can match the most advanced known concepts at will.

Some research Papers that use this

Patrick Albert, Laurent Henocque, Mathias Kleiner, "An end-to-end configuration-based framework for automatic SWS composition", in: Proceedings of the 20th IEEE Intl Conference on Tools with Artificial Intelligence, ICTAI'08, pp. 351--358, Dayton, OHIO, USA, November, 2008. pdf

Barry Norton, Carlos Pedrinaci, Jens Lemcke, Mathias Kleiner, Laurent Henocque, Gabriela Vulcu, "Ontology for Web Services Choreography and Orchestration - DIP Deliverable D3.9", pp. 1--76, March 20, 2007. pdf (also in the DIP Project's context)

Mathias Kleiner, "Contribution to the use of Constraint Programming for Finite Model Search in Artificial Intelligence", in: Thèse de Doctorat de l'Université de la Méditerranée-Aix-Marseille II, pp. 1--206, Marseille, France, Novembre, 2007.pdf

Mathieu Estratat, Laurent Henocque, "An Intuitive Tool for Constraint Based Grammars", in: Revised Selected and Invited Papers, Constraint Solving and Language Processing, First International Workshop, CSLP 2004, edited by Henning Christiansen, Peter Rossen Skadhauge, Jorgen Villadsen, publisher: Springer, series: Lecture Notes in Computer Science, volume 3438, pp. 121--139, Copenhagen, Denmark, September, 2005.pdf

Related tools

Alloy4 is a validation tool for object oriented specifications that uses a simple relational language that can be viewed as strict a subset of Z. The tool translates bounded specifications to SAT using KodKod.

Use provides both OCL invariant checking and snapshot (unbounded finite instance) generation of UML+OCL language.

The Community Z Tools sourceforge initiative also provides for continuous delelopment of Z related tools and apis.