
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Brendan Mahony, Jin Song Dong, "Timed Communicating Object Z," IEEE Transactions on Software Engineering, vol. 26, no. 2, pp. 150177, February, 2000.  
BibTex  x  
@article{ 10.1109/32.841115, author = {Brendan Mahony and Jin Song Dong}, title = {Timed Communicating Object Z}, journal ={IEEE Transactions on Software Engineering}, volume = {26}, number = {2}, issn = {00985589}, year = {2000}, pages = {150177}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.841115}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Timed Communicating Object Z IS  2 SN  00985589 SP150 EP177 EPD  150177 A1  Brendan Mahony, A1  Jin Song Dong, PY  2000 KW  Software/system specification KW  formal methods KW  realtime systems KW  concurrency KW  objectoriented modeling KW  Z KW  CSP. VL  26 JA  IEEE Transactions on Software Engineering ER   
Abstract—This paper describes a timed, multithreaded object modeling notation for specifying realtime, 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 realtime 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 wellsuited 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 realtime.
[1] M. Abadi and L. Lamport, “An OldFashioned Recipe for Real Time,” ACM Trans. Programming Languages, vol. 15, no. 5, pp. 1,5431571, 1991.
[2] B. Auernheimer and R.A. Kemmerer, “Rtaslan: A Specification Language for RealTime 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. 87152, 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. AddisonWesley, 1988.
[8] A. CoenPorisini, C. Ghezzi, and R. Kemmerer, “Specification of RealTime Systems Using ASTRAL,” Technical Report 9630, 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 9410, Department of Computer and Information Science, Univ. of Mississippi, 1994.
[10] J.S. Dong, “Living with Free Type and Class Union,” Proc. 1995 AsiaPacific Software Eng. Conf. (APSEC '95), pp. 304–312, Dec. 1995.
[11] J.S. Dong, J. Colton, and L. Zucconi, “A Formal Object Approach to RealTime Specification,” Proc. Third AsiaPacific Software Eng. Conf. (APSEC '96), Dec. 1996.
[12] J. S. Dong and R. Duke, “The Geometry of Object Containment,” ObjectOriented 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 911, Software Verification Research Centre, Australia, 1991.
[17] R. Duke and G. Rose, “Modeling Object Identity,” Proc. 16th Australian Computer Science Conf. (ACSC16), pp. 93–100, Feb. 1993.
[18] R. Duke and G. Rose, Formal ObjectOriented Specification. Academic Press, 1998.
[19] R. Duke, G. Rose, and G. Smith, “ObjectZ, A Specification Language Advocated for the Description of Standards,” Computer Standards and Interfaces, vol. 17, pp. 511533, 1995.
[20] C. Fidge, P. Kearney, and M. Utting, "A Formal Method for Building Concurrent RealTime Software," IEEE Software, Vol. 14, No. 2, Mar./Apr. 1997, pp. 99106.
[21] C. Fisher, “CSPOZ  A Combination of CSP and ObjectZ,” Proc. Second IFIP Int'l Conf. Formal Methods for Open ObjectBased Distributed Systems, pp. 423438, 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 RealTime Systems," J. Systems and Software, vol. 12, no. 2, pp. 107123, 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 9624, Software Verification Research Centre, School of Information Technology, Univ. of Queensland, Brisbane, Australia, July 1996.
[34] M.B. Josephs, “A StateBased 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. 872923, 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 9505, 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. PrenticeHall, 1997.
[45] S. Schneider, “Correctness and Communication in RealTime Systems,” PhD thesis, Oxford University Computing Laboratory, Programming Research Group, 1990. Available as Technical Monograph PRG84.
[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 ObjectZ and CSP for the Specification of Concurrent Systems,” Proc. Formal Methods Europe (FME '97), Sept. 1997.
[50] K. Taguchi and K. Araki, “The StateBased 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 RealTime Systems: An Elevator Case Study,” Technical Report 9304, Computer Science Dept., Univ. of British Columbia, 1993.