An Object-Z Specification of a Petrol Supply System

Abstract:

As modern complex computer systems become increasingly sophisticated and data-intensive, people have long recognized the importance of precisely and unambiguously specifying them with formal methods. 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. First, we informally describe the syntax and semantics of Object-Z, highlighting those features that facilitate decomposing a large system into a collection of underlying 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.

• Periodical: Applied Mechanics and Materials (Volumes 427-429)
• Pages: 2349-2353
• DOI: https://doi.org/10.4028/www.scientific.net/AMM.427-429.2349
• Online since: September 2013
• Authors: Yang Ping Li*, Wei Quan Zhao, Xiao Rui Wei
• Keywords: Formal Methods, Object-Oriented Modeling, Object-Z, System Specification

References

[1] J. Bicarregui, J. Fitzgerald, P. Larsen, and J. Woodcock, FM 2009: Formal Methods. Springer, 2009, ch. Industrial Practice in Formal Methods: A Review, p.810–813.

DOI: 10.1007/978-3-642-05089-3_52

[2] M. Henson, S. Reeves, and J. Bowen, Z logic and its consequences, Computing and Informatics, vol. 22, no. 3-4, p.381–415, (2012).

[3] J. Dong, R. Duke, and G. Rose, An object-oriented approach to thesemantics of programming languages, in Proceedings of the 17-th Annual Computer Science Conference, 1994, p.767–775.

[4] G. Rose and R. Duke, Object-Oriented Specification Case Studies. Prentice Hall International, 1993, ch. An Object-Z Specification of a Mobile Phone System, p.110–129.

[5] J. Sun, H. Wang, and T. Hu, Design software architecture models using ontology, in Proceedings of the 23rd International Conference on Software Engineering & Knowledge Engineering, 2011, p.191–196.

[6] A. Felfernig, F. Reinfrank, and G. Ninaus, Foundations of Intelligent Systems. Springer-Verlag, 2012, ch. Resolving Anomalies in Configuration Knowledge Bases, p.311–320.

DOI: 10.1007/978-3-642-34624-8_36

[7] T. Hu, C. L. Tan, Y. Tang, S. Y. Sung, H. Xiong, and C. Qu, Co-clustering bipartite with pattern preservation for topic extraction, International Journal on Artificial Intelligence Tools, vol. 17, no. 1, p.87–107, (2008).

DOI: 10.1142/s0218213008003790

[8] M. Shahbaz, K. C. Shashidhar, and R. Eschbach, Iterative refinement of specification for component based embedded systems, in Proceedings of the 2011 International Symposium on Software Testing and Analysis, 2011, p.276–286.

DOI: 10.1145/2001420.2001454