| UMLtoCSP |
|---|
| Presentation |
| Download |
| Screenshots |
| Usage |
| Examples |
| Links |
| Quick links |
|---|
| GRES Home |
| GRES Wiki |
Verification of operations
The original version of UMLtoCSP supports only OCL invariants. This page, under construction, is devoted to the verification of OCL pre/postconditions of operations.
It is possible to check several quality notions of pre/postconditions using UMLtoCSP. For instance, it is possible to check whether a precondition is satisfiable (applicability), whether the postcondition is satisfiable (weak/strong executability), whether any post-state violates system invariants (correctness preserving), ...
A version of UMLtoCSP implementing these features is available in the following link:
| UMLtoCSP - Latest release | |
|---|---|
| File: | UMLtoCSP.ZIP [ ZIP file ] |
| Version date: | Sept 26, 2008 |
| What's new?: | Bug fixes, Improved command-line interface |
| Platforms: | Windows and Linux |
Screenshots
Click on the following screenshots to enlarge the picture:
|
|
| Selection of correctness properties | Snapshot proving applicability of a precondition. |
Examples
A simple model of an e-commerce application, with customers, products and sales:
- UML class diagrams [ XMI, PNG ]
- OCL constraints, including two invariants and three operations [ text file ]
- ECLiPSe code generated for this problem [ text file ]
- Counterexample proving that the operation
addSaleLinedoes not preserve correctness: this initial state [ PNG ] produces this final state [ PNG ] which does not satisfy the invariantminStock.
