Integrating a formal method into a software engine

Authors: Michael Möller ErnstRüdiger Olderog Holger Rasch Heike Wehrheim

Publish Date: 2007/07/19

Volume: 20, Issue: 2, Pages: 161-204

PDF Link

Abstract

We describe how CSPOZ a formal method combining the process algebra CSP with the specification language ObjectZ can be integrated into an objectoriented software engineering process employing the UML as a modelling and Java as an implementation language The benefit of this integration lies in the rigour of the formal method which improves the precision of the constructed models and opens up the possibility of 1 verifying properties of models in the early design phases and 2 checking adherence of implementations to modelsThe envisaged application area of our approach is the design of distributed reactive systems To this end we propose a specific UML profile for reactive systems The profile contains facilities for modelling components their interfaces and interconnections via synchronous/broadcast communication and the overall architecture of a system The integration with the formal method proceeds by generating a significant part of the CSPOZ specification from the initially developed UML model The formal specification is on the one hand the starting point for verifying properties of the model for instance by using the FDR model checker On the other hand it is the basis for generating contracts for the final implementation Contracts are written in the Java Modeling Language JML complemented by CSPjassda an assertion language for specifying orderings between method invocations A set of tools for runtime checking can be used to supervise the adherence of the final Java implementation to the generated contracts

Keywords: