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:
Click on the following screenshots to enlarge the picture:
A simple model of an e-commerce application, with customers, products and sales: