Linking CSP-OZ with UML and Java: A Case Study

Abstract. We describe how CSP-OZ, an integrated formal method combining the process algebra CSP with the specification language Object-Z, can be linked to standard software engineering languages, viz. UML and Java. Our aim is to generate a significant part of the CSP-OZ specification from an initially developed UML model using a UML profile for CSP-OZ, and afterwards transform the formal specification into assertions written in the Java Modelling Language JML complemented by CSPjassda . The intermediate CSP-OZ specification serves to verify correctness of the UML model, and the assertions control at runtime the adherence of a Java implementation to these formal requirements. We explain this approach using the case study of a “holonic manufacturing system” in which coordination of transportation and processing is distributed among stores, machine tools and agents without central control. Keywords. CSP, Object-Z, UML, Java, assertions, runtime checking

• Type: Conference
• Year: 2004
• Where: IFM
• Authors: Michael Möller, Ernst-Rüdiger Olderog, Holger Rasch, Heike Wehrheim
• Keywords: CSP-OZ Specification, IFM 2004, Intermediate Csp-oz Specification, UML Model