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

9 years 3 months ago
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
Michael Möller, Ernst-Rüdiger Olderog, H
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where IFM
Authors Michael Möller, Ernst-Rüdiger Olderog, Holger Rasch, Heike Wehrheim
Comments (0)