Analysis by contract: UML with attitude!

Summary form only given, as follows. At the heart of the Unified Modeling Language (UML) are a number of visual modeling notations for describing classes, states, and so on. The UML also contains an Object Constraint Language, OCL, for adding precision to models. OCL can be used to add preconditions, postconditions and invariants to classes or types, allowing the precision of design by contract to be applied at any level of abstraction. This tutorial will introduce OCL, and show it in action on a small case study. It will emphasize how abstraction need not lead to a loss of precision, and how precision can allow powerful cross-checking of models, thereby improving the analysis process. Precision will be increasingly important as the software industry moves further towards component-based development. The case study will emphasize: why types are a suitable analysis-level abstraction; how type models can provide a vocabulary for behavior modeling; how type models can be improved with invariants; how state modeling can support analysis-level modeling; how state models and type models can be cross-checked; how behavior can be expressed using preconditions and postconditions.