HOL-OCL

Archived

A collection of (toy) examples using OCL.

This repository has been archived on 2024-04-22. You can view files and clone it, but cannot push or open issues or pull requests.

Go to file

Achim D. Brucker d031448347 Cleanup: outdated commented stuff.		2016-10-05 08:00:59 +01:00
calendar	Added class diagram as PDF.	2016-10-03 00:50:41 +01:00
company	Cleanup: outdated commented stuff.	2016-10-05 08:00:24 +01:00
controller_calendar	Added simple calender model using ControllerUML.	2016-10-03 06:39:32 +01:00
digraph	Cleanup: outdated commented stuff.	2016-10-05 08:00:29 +01:00
ebank	Cleanup: outdated commented stuff.	2016-10-05 08:00:33 +01:00
health_system	Added small health system example.	2016-10-03 04:19:55 +01:00
invoicing_orders	The InvoicingOrders system.	2016-10-05 00:38:00 +01:00
isp	Added ISP example.	2016-10-02 22:10:25 +01:00
mini_company	Cleanup: outdated commented stuff.	2016-10-05 08:00:37 +01:00
priority_queue	Added simple priority queue.	2016-10-04 10:12:05 +01:00
rbt	Red-Black-Tree model.	2016-10-05 01:26:15 +01:00
royals_and_loyals	Cleanup: outdated commented stuff.	2016-10-05 08:00:42 +01:00
simple	Cleanup: outdated commented stuff.	2016-10-05 08:00:47 +01:00
simple_chair	Cleanup: outdated commented stuff.	2016-10-05 08:00:53 +01:00
simple_filesystem	Added a simple filesystem model.	2016-10-03 08:11:30 +01:00
stack	Cleanup: outdated commented stuff.	2016-10-05 08:00:59 +01:00
vehicles	Added simple vehicle example.	2016-10-03 04:31:24 +01:00
LICENSE	Changed default license.	2016-10-02 13:57:54 +01:00
README.md	Red-Black-Tree model.	2016-10-05 01:26:15 +01:00

README.md

ocl-examples

A collection of (toy) examples using OCL that demonstrate the use of OCL in the context of UML as well as SecureUML models. Most of the models were developed in the context of the HOL-OCL and SecureUML projects.

Models

Controller Calendar: A simple calendar/meeting model using ControllerUML.
Calendar: A simple calendar/meeting model.
Company: A simple company model, inspired by the OCL standard.
Digraph: A simple tree like (recursive) data structure.
E-Bank: A simple eBank/Accounting model.
Health System: A simple health system.
Invoicing Orders: A simple invoicing model.
ISP: A simple example of an ISP.
Mini Company: A tiny company example modelling a management hierarchy.
Priority Queue: A simple priority queue model.
Red-Black-Tree: A UML/OCL model of red-black-trees.
Royals and Loyals: The famous royals-and-loyals example.
Simple: A very simple toy example showing a few OCL syntax variations.
Simple Chair: A simple conference management system.
Simple Filesystem: A simple POSIX-like fileystem model.
Stack: A simple stack.
Vehicles: A simple model of vehicles and driver's licenses.

Team

Achim D. Brucker

License

This project is licensed under a 2-clause BSD license.

Publications

Achim D. Brucker and Burkhart Wolff. Semantics, Calculi, and Analysis for Object-oriented Specifications. In Acta Informatica, 46 (4), pages 255-284, 2009. https://www.brucker.ch/bibliography/abstract/brucker.ea-semantics-2009 doi: 10.1007/s00236-009-0093-8
Achim D. Brucker and Burkhart Wolff. An Extensible Encoding of Object-oriented Data Models in HOL. In Journal of Automated Reasoning, 41, pages 219-249, 2008. https://www.brucker.ch/bibliography/abstract/brucker.ea-extensible-2008-b doi: 10.1007/s10817-008-9108-3
Achim D. Brucker. An Interactive Proof Environment for Object-oriented Specifications. ETH Zurich,2007. ETH Dissertation No. 17097. https://www.brucker.ch/bibliography/abstract/brucker-interactive-2007
Achim D. Brucker, Jürgen Doser, and Burkhart Wolff. A Model Transformation Semantics and Analysis Methodology for SecureUML. In MoDELS 2006: Model Driven Engineering Languages and Systems. Lecture Notes in Computer Science (4199), pages 306-320, Springer-Verlag, 2006. https://www.brucker.ch/bibliography/abstract/brucker.ea-transformation-2006 doi: 10.1007/11880240_22