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.
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 :
- Language design (a language is a model - a model is a language)
- Meta modeling
- Ontology specification
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
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.
This sourceforge project makes freely accessible latex templates originally used in The Marseille Constraint based Configuration Group research papers.
About the author
Why "Zoomdea"? Z - OO - MDE - MDA