doi: 10.4304/jsw.9.7.1707-1717
Specifying Complex Systems in Object-Z: A Case Study of Petrol Supply Systems
- 1 Dongguan University of Technology, China
- 2 South Texas College, USA
Abstract
As modern complex systems become increasingly large, sophisticated, feature-rich and data-intensive, people have recognized the importance of precisely and unambigu- ously specifying them with formal methods for a number of years. This paper advocates the use of Object-Z, a formal specification language, in the description of complex systems. Object-Z is an extension to the Z language to facilitate specification in an object-oriented style. The notation Object- Z builds on Z’s strengths in modeling complex data and algorithms, and on its new class structuring’s strengths in succinctly specifying the various relationships and commu- nication between objects in a large system. In detail, first we describe informally the syntax and semantics of Object- Z, highlighting those features that facilitate decomposing a large system into a collection of interacting objects and thus separating concerns. Then, we demonstrate the use of Object-Z by presenting a case study of a petrol supply system, illustrating how the system runs by communicating the constituent objects. Finally, we discuss several issues we encountered in this exercise, which may serve as feedback to the development of Object-Z.
Keywords
- Object-Z;
- object-oriented
- modeling;
- form
How to Cite
Yangping Li, Xiaoheng Pan, Tianming Hu, Sam Yuan Sung, and Huaqiang Yuan, "Specifying Complex Systems in Object-Z: A Case Study of Petrol Supply Systems," Journal of Software, vol. 9, no. 7, pp. 1707-1717, 2014. https://doi.org/ 10.4304/jsw.9.7.1707-1717
Copyright & License
Copyright © 2014 by the authors. This is an open access article distributed under the Creative Commons Attribution License which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited (CC BY 4.0).