This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Timed Communicating Object Z
February 2000 (vol. 26 no. 2)
pp. 150-177

Abstract—This paper describes a timed, multithreaded object modeling notation for specifying real-time, concurrent, and reactive systems. The notation Timed Communicating Object Z (TCOZ) builds on Object Z's strengths in modeling complex data and algorithms, and on Timed CSP's strengths in modeling process control and real-time interactions. TCOZ is novel in that it includes timing primitives, properly separates process control and data/algorithm issues and supports the modeling of true multithreaded concurrency. TCOZ is particularly well-suited for specifying complex systems whose components have their own thread of control. The expressiveness of the notation is demonstrated by a case study in specifying a multilift system that operates in real-time.

[1] M. Abadi and L. Lamport, “An Old-Fashioned Recipe for Real Time,” ACM Trans. Programming Languages, vol. 15, no. 5, pp. 1,543-1571, 1991.
[2] B. Auernheimer and R.A. Kemmerer, “Rt-aslan: A Specification Language for Real-Time Systems,” IEEE Trans. Software Eng., vol. 12, no. 9, Sept. 1986.
[3] R.J.R. Back and J. von Wright, “Refinement Calculus, Part II: Parallel and Reactive Programs,” Stepwise Refinement. J.W. de Bakker, W.P. de Roever, and G. Rozenberg, eds., Springer Verlag, 1990.
[4] M. Benjamin, “A Message Passing System: An Example of Combining CSP and Z,” Z User Workshop: Proc. Fourth Ann. Z User Meeting, pp. 221–228, Dec. 1989
[5] G. Berry and G. Gonthier, "The ESTERELSynchronous Programming Language: Design, Semantics, Implementation," Science of Computer Programming, vol. 19, no. 2, pp. 87-152, 1992.
[6] M.J. Butler, “A CSP Approach to Action Systems,” PhD thesis, Wolfson College, Oxford University, 1992.
[7] K.M. Chandy and J. Misra, Parallel Program Design—A Foundation. Addison-Wesley, 1988.
[8] A. Coen-Porisini, C. Ghezzi, and R. Kemmerer, “Specification of Real-Time Systems Using ASTRAL,” Technical Report 96-30, Computer Science Dept., Univ. of California, Santa Barbara, Jan. 1997.
[9] H.C. Cunningham, V.R. Shan, and S. Shen, “Devising a Formal Specification for an Elevator Controller,” Technical Report TR 94-10, Department of Computer and Information Science, Univ. of Mississippi, 1994.
[10] J.S. Dong, “Living with Free Type and Class Union,” Proc. 1995 Asia-Pacific Software Eng. Conf. (APSEC '95), pp. 304–312, Dec. 1995.
[11] J.S. Dong, J. Colton, and L. Zucconi, “A Formal Object Approach to Real-Time Specification,” Proc. Third Asia-Pacific Software Eng. Conf. (APSEC '96), Dec. 1996.
[12] J. S. Dong and R. Duke, “The Geometry of Object Containment,” Object-Oriented Systems, vol. 2, no. 1, pp. 41–63, Mar. 1995.
[13] J.S. Dong and B.P. Mahony, “Active Objects in TCOZ,” Proc. Second Int'l Conf. Formal Eng. Methods (ICFEM '98), pp. 16–25, 1998.
[14] J.S. Dong, G. Rose, and R. Duke, “The Role of Secondary Attributes in Formal Object Modeling” Proc. First IEEE Int'l Conf. Eng. Complex Computer Systems (ICECCS '95), pp. 31–38, Nov. 1995.
[15] J.S. Dong, L. Zucconi, and R. Duke, “Specifying Parallel and Distributed Systems in Object Z,” Second Int'l Workshop Software Eng. for Parallel and Distributed Systems, pp. 140–149, 1997.
[16] R. Duke, P. King, G. Rose, and G. Smith, “The Object Z Specification Language: Version 1,” Technical Report 91-1, Software Verification Research Centre, Australia, 1991.
[17] R. Duke and G. Rose, “Modeling Object Identity,” Proc. 16th Australian Computer Science Conf. (ACSC-16), pp. 93–100, Feb. 1993.
[18] R. Duke and G. Rose, Formal Object-Oriented Specification. Academic Press, 1998.
[19] R. Duke, G. Rose, and G. Smith, “Object-Z, A Specification Language Advocated for the Description of Standards,” Computer Standards and Interfaces, vol. 17, pp. 511-533, 1995.
[20] C. Fidge, P. Kearney, and M. Utting, "A Formal Method for Building Concurrent Real-Time Software," IEEE Software, Vol. 14, No. 2, Mar./Apr. 1997, pp. 99-106.
[21] C. Fisher, “CSP-OZ - A Combination of CSP and Object-Z,” Proc. Second IFIP Int'l Conf. Formal Methods for Open Object-Based Distributed Systems, pp. 423-438, July 1997.
[22] I. R. Forman, “Design by Decomposition of Multiparty Interactions in Raddle87,” Proc. Fifth IEEE Int'l Workshop Software Specification and Design (IWSSD'89), pp. 2–10, 1989.
[23] A.J. Galloway, “Integrated Formal Methods with Richer Methodological Profiles for the Development of Multiperspective Systems,” PhD thesis, Univ. of Teesside, School of Computing and Mathematics, Aug. 1996.
[24] A.J. Galloway and W.J. Stoddart, “An Operational Semantics for ZCCS,” Proc. IEEE Int'l Conf. Formal Eng. Methods (ICFEM '97), pp. 272–282, Nov. 1997.
[25] C. George, P. Haff, K. Havelund, A.E. Haxthausen, R. Milne, C.B. Nielson, S. Prehn, and K.R. Wagner, The Raise Specification Language. New York: Prentice Hall, 1992.
[26] C. Ghezzi, D. Mandriolli, and A. Morzenti, "Trio: A Logic Language for Executable Specifications of Real-Time Systems," J. Systems and Software, vol. 12, no. 2, pp. 107-123, May 1990.
[27] I.J. Hayes and B.P. Mahony, “Using Units of Measurement in Formal Specifications,” Formal Aspects of Computing vol. 7, no. 3, 1995.
[28] J. He, “Process Simulation and Refinement,” Formal Aspects of Computing, vol. 1, no. 3, pp. 229–241, 1989.
[29] C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, Englewood Cliffs, N.J., 1985.
[30] Units of Measurement: Handbook on Int'l Standards for Units of Measurement. Geneva: Int'l Organization for Standardization, 1979.
[31] “ISO,” SC21/WG7 Working Draft on Enhancements to LOTOS, ISO Working Group 7, Dec. 1997.
[32] “ISO 8807,” LOTOS–A Formal Description Technique Based on the Temporal Ordering of Observational Behavior, 1989.
[33] W. Johnston, “A Type Checker for Object Z,” Technical Report 96-24, Software Verification Research Centre, School of Information Technology, Univ. of Queensland, Brisbane, Australia, July 1996.
[34] M.B. Josephs, “A State-Based Approach to Communicating Processes,” Distributed Computing, vol. 3, pp. 9–18, 1988.
[35] L. Lamport and S. Owicki, "The Temporal Logic of Actions," ACM Trans. Programming Languages and Systems, vol. 16, pp. 872-923, May 994.
[36] L. Lamport and L.C. Paulson, “Should Your Specification Language Be Typed?” Technical Report 147, Systems Research Center, 1997.
[37] B.P. Mahony and J.S. Dong, “Overview of the Semantics of TCOZ,” Proc. IFM '99: Integrated Formal Methods, pp. 66–85, June 1999.
[38] B.P. Mahony, “Networks of Predicate Transformers,” Technical Report 95-05, Software Verification Research Centre, Department of Computer Science, Univ. of Queensland, St. Lucia, Australia, Feb. 1995.
[39] B.P. Mahony and J. S. Dong, “Blending Object Z and Timed CSP: An Introduction to TCOZ,” Proc. 20th Int'l Conf. Software Eng. (ICSE'98), Apr. 1998.
[40] B.P. Mahony and J.S. Dong, “Network Topology and a Case Study in TCOZ,” Proc. ZUM '98 11th Int'l Conf. Z Users,, vol. 1,493, Sept. 1998.
[41] B.P. Mahony and I.J. Hayes, “A Case Study in Timed Refinement: A Mine Pump,” IEEE Trans. Software Eng., vol. 18, no. 9, pp. 817–826, Sept. 1992.
[42] M. Mislove, A. Roscoe, and S. Schneider, “Fixed Points without Completeness,” Theoretical Computer Science, vol. 138, pp. 273–314, 1995.
[43] C.C. Morgan, Programming from Specifications, second edition. Englewood Cliffs, N.J.: Prentice Hall, 1994.
[44] A.W. Roscoe, Theory and Practice of Concurrency. Prentice-Hall, 1997.
[45] S. Schneider, “Correctness and Communication in Real-Time Systems,” PhD thesis, Oxford University Computing Laboratory, Programming Research Group, 1990. Available as Technical Monograph PRG-84.
[46] S. Schneider and J. Davies, “A Brief History of Timed CSP,” Theoretical Computer Science, vol. 138, 1995.
[47] M.D. Schwartz and N.M. Delisle, “Specifying a Lift Control System with CSP,” Proc. Fourth IEEE Int'l Workshop Software Specification and Design (IWSSD '87), pp. 21–27, Apr. 1987.
[48] G. Smith, “A Fully Abstract Semantics of Classes for Object Z,” Formal Aspects of Computing, vol. 7, no. 3, pp. 289–313, 1995.
[49] G. Smith, “A Semantic Integration of Object-Z and CSP for the Specification of Concurrent Systems,” Proc. Formal Methods Europe (FME '97), Sept. 1997.
[50] K. Taguchi and K. Araki, “The State-Based CCS Semantics for Concurrent Z Specification,” Proc. IEEE Int'l Conf. Formal Eng. Methods (ICFEM '97), pp. 283–292, Nov. 1997.
[51] J.C.P. Woodcock, S. King, and I.H. Sorensen, “Mathematics for Specification and Design: The Problem with Lifts,” Proc. Fourth IEEE Int'l Workshop Software Specification and Design (IWSSD '87), pp. 265–268, 1987.
[52] Y Zhang and A.K. Mackworth, “Design and Analysis of Embedded Real-Time Systems: An Elevator Case Study,” Technical Report 93-04, Computer Science Dept., Univ. of British Columbia, 1993.

Index Terms:
Software/system specification, formal methods, real-time systems, concurrency, object-oriented modeling, Z, CSP.
Citation:
Brendan Mahony, Jin Song Dong, "Timed Communicating Object Z," IEEE Transactions on Software Engineering, vol. 26, no. 2, pp. 150-177, Feb. 2000, doi:10.1109/32.841115
Usage of this product signifies your acceptance of the Terms of Use.