Abstract
An automatic manufacturing system serves as a case study for the applicability of an integrated formal method to the specification of software systems. The formal method chosen is CSP-OZ, an integration of the state-oriented formalism Object-Z with the process algebra CSP. The practicability as well as limitations of CSP-OZ are studied. We furthermore employ a graphical notation (class diagrams) from the Unified Modelling Language to describe the architectural view of the system. The correctness of the obtained specification is checked by a translation into the input language of the CSP model checker FDR and a following property check.
This work was partially funded by the Leibniz Programme of the German Research Council (DFG) under grant Ol 98/1-1.
Chapter PDF
References
R. Duke, G. Rose, and G. Smith. Object-Z: A specification language advocated for the description of standards. Computer Standards and Interfaces, 17:511–533, 1995.
Formal Systems (Europe) Ltd. Failures-Divergence Refinement: FDR2 User Manual, Oct 1997.
C. Fischer. CSP-OZ: A combination of Object-Z and CSP. In H. Bowman and J. Derrick, editors, Formal Methods for Open Object-Based Distributed Systems (FMOODS’ 97), volume 2, pages 423–438. Chapman & Hall, 1997.
C. Fischer and H. Wehrheim. Model-checking CSP-OZ specifications with FDR. In K. Araki, A. Galloway, and K. Taguchi, editors, Proceedings of the 1st International Conference on Integrated Formal Methods (IFM), pages 315–334. Springer, 1999.
J.F. Groote and A. Ponse. Proof theory for μ-CRL: A language for processes with data. In Semantics of specification languages, Workshops in Computing. Springer, 1993.
A. J. Galloway and W. Stoddart. An operational semantics for ZCCS. In M. Hinchey and Shaoying Liu, editors, Int. Conf. of Formal Engineering Methods (ICFEM). IEEE, 1997.
C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
B. P. Mahony and J.S. Dong. Blending Object-Z and Timed CSP: An introduction to TCOZ. In The 20th International Conference on Software Engineering (ICSE’98), pages 95–104. IEEE Computer Society Press, April 1998.
A. Mota and A. Sampaio. Model-checking CSP-Z. In Proceedings of the European Joint Conference on Theory and Practice of Software, volume 1382 of LNCS, pages 205–220, 1998.
Object Management Group. OMG Unified Modeling Language Specification, June 1999. version 1.3.
J. Quemada, editor. Revised working draft on enhancements to LOTOS (V4). ISO, 1996.
A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1997.
G. Smith. A semantic integration of Object-Z and CSP for the specification of concurrent systems. In J. Fitzgerald, C. B. Jones, and P. Lucas, editors, Proceedings of FME 1997, volume 1313 of LNCS, pages 62–81. Springer, 1997.
G. Smith. The Object-Z Specification Language. Kluwer Academic Publisher, 2000.
J. M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall International Series in Computer Science, 2nd edition, 1992.
B. Selic and J. Rumbaugh. Using UML for modeling complex real-time systems. Technical report, ObjecTime, 1998.
K. Taguchi and K. Araki. Specifying concurrent systems by Z + CCS. In International Symposium on Future Software Technology (ISFST), pages 101–108, 1997.
E. Westkämper, M. Höpf, and C. Schaefier. Holonic manufacturing systems. In Lake Tahoe HMS Consortium, editor, Holonic manufacturing systems, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wehrheim, H. (2000). Specification of an Automatic Manufacturing System: A Case Study in Using Integrated Formal Methods. In: Maibaum, T. (eds) Fundamental Approaches to Software Engineering. FASE 2000. Lecture Notes in Computer Science, vol 1783. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46428-X_23
Download citation
DOI: https://doi.org/10.1007/3-540-46428-X_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67261-6
Online ISBN: 978-3-540-46428-0
eBook Packages: Springer Book Archive