research-article

Timed Communicating Object Z

Authors:

Brendan Mahony,

Jin Song DongAuthors Info & Claims

IEEE Transactions on Software Engineering, Volume 26, Issue 2

Pages 150 - 177

https://doi.org/10.1109/32.841115

Published: 01 February 2000 Publication History

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.

References

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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 Esterel Synchronous Programming Language: Design, Semantics, Implementation,” Science of Computer Programming, vol. 19, no. 2, pp. 87–152, Nov. 1992.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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, no. 511–533, 1995.

Digital Library

[20]

C. Fidge P. Kearney and M. Utting, “A Formal Method for Building Concurrent Real-Time Software,” IEEE Software, vol. 14, no. 2, 1997.

Digital Library

[21]

C. Fischer, “CSP-OZ: A Combination of Object Z and CSP,” Formal Methods for Open Object-Based Distributed Systems (FMOODS'97), vol. 2, pp. 423–438, 1997.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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. Mandrioli and A. Morzenti, “Trio: A Logic Language for Executable Specifications of Real-Time System,” J. Systems and Software, June 1990.

Digital Library

[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, 1985.

Digital Library

[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.

Digital Library

[35]

L. Lamport, “The Temporal Logic of Actions,” “ACM Trans. Programming Languages and Systems,” vol. 16, pp. 872–923, 1994.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[42]

M. Mislove A. Roscoe and S. Schneider, “Fixed Points without Completeness,” Theoretical Computer Science, vol. 138, pp. 273–314, 1995.

Digital Library

[43]

C.C. Morgan, Programming from Specifications, second ed. Prentice Hall, 1994.

Digital Library

[44]

A.W. Roscoe, Theory and Practice of Concurrency. Prentice-Hall, 1997.

Digital Library

[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.

Digital Library

[46]

S. Schneider and J. Davies, “A Brief History of Timed CSP,” Theoretical Computer Science, vol. 138, 1995.

Digital Library

[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. FME '97: Industrial Benefit of Formal Methods, Sept. 1997.

Digital Library

[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.

Digital Library

[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.

Digital Library

Cited By

Shi LZhao YLiu YSun JDong JQin S(2018)A UTP semantics for communicating processes with shared variables and its formal encoding in PVSFormal Aspects of Computing10.1007/s00165-018-0453-730:3-4(351-380)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s00165-018-0453-7
Ni SZhuang YGu JHuo Y(2016)A formal model and risk assessment method for security-critical real-time embedded systemsComputers and Security10.1016/j.cose.2016.01.00558:C(199-215)Online publication date: 1-May-2016
https://dl.acm.org/doi/10.1016/j.cose.2016.01.005
Nooraei Abadeh MMirian-Hosseinabadi S(2015)Delta-based regression testingJournal of Software: Evolution and Process10.5555/3028565.302856727:12(913-952)Online publication date: 1-Dec-2015
https://dl.acm.org/doi/10.5555/3028565.3028567
Show More Cited By

Index Terms

Timed Communicating Object Z
1. Computer systems organization
  1. Embedded and cyber-physical systems
  2. Real-time systems
2. Software and its engineering
  1. Software creation and management
    1. Software development process management
      1. Software development methods

Recommendations

A Formal Framework for ASTRAL Intralevel Proof Obligations

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL ...
Specification, Refinement and Verification of Concurrent Systems—An Integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of ...
A formal data-model of the CORBA security service

We use the formal language Z to specify and analyze the security service of CORBA. In doing so, we tackle the problem of how one can apply lightweight formal methods to improve the precision and aid the analysis of a substantial, informal specification. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image IEEE Transactions on Software Engineering

IEEE Transactions on Software Engineering Volume 26, Issue 2

February 2000

95 pages

ISSN:0098-5589

Editor:
Anneliese von Mayrhauser
Colorado State Univ., Fort Collins

Issue’s Table of Contents

Copyright © Copyright © 2000 IEEE. All Rights Reserved.

Publisher

IEEE Press

Publication History

Published: 01 February 2000

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

40
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Shi LZhao YLiu YSun JDong JQin S(2018)A UTP semantics for communicating processes with shared variables and its formal encoding in PVSFormal Aspects of Computing10.1007/s00165-018-0453-730:3-4(351-380)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s00165-018-0453-7
Ni SZhuang YGu JHuo Y(2016)A formal model and risk assessment method for security-critical real-time embedded systemsComputers and Security10.1016/j.cose.2016.01.00558:C(199-215)Online publication date: 1-May-2016
https://dl.acm.org/doi/10.1016/j.cose.2016.01.005
Nooraei Abadeh MMirian-Hosseinabadi S(2015)Delta-based regression testingJournal of Software: Evolution and Process10.5555/3028565.302856727:12(913-952)Online publication date: 1-Dec-2015
https://dl.acm.org/doi/10.5555/3028565.3028567
Siru Ni Yi Zhuang Zining Cao Xiangying Kong (2015)Modeling Dependability Features for Real-Time Embedded SystemsIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2014.232071412:2(190-203)Online publication date: 1-Mar-2015
https://dl.acm.org/doi/10.1109/TDSC.2014.2320714
Sun JLiu YDong JLiu YShi LAndré É(2013)Modeling and verifying hierarchical real-time systems using stateful timed CSPACM Transactions on Software Engineering and Methodology10.1145/2430536.243053722:1(1-29)Online publication date: 4-Mar-2013
https://dl.acm.org/doi/10.1145/2430536.2430537
Luu ASun JLiu YDong JLi XQuan T(2012)SeVeFrontiers of Computer Science in China10.5555/2125163.21251866:1(57-75)Online publication date: 1-Feb-2012
https://dl.acm.org/doi/10.5555/2125163.2125186
Kaur AGulati SSingh SMeghanathan NWozniak M(2012)A comparative study of two formal specification languagesProceedings of the Second International Conference on Computational Science, Engineering and Information Technology10.1145/2393216.2393304(524-531)Online publication date: 26-Oct-2012
https://dl.acm.org/doi/10.1145/2393216.2393304
Cavalcanti AClayton PO’Halloran C(2011)From control law diagrams to Ada via CircusFormal Aspects of Computing10.1007/s00165-010-0170-323:4(465-512)Online publication date: 1-Jul-2011
https://dl.acm.org/doi/10.1007/s00165-010-0170-3
Beg AButterfield A(2010)Modelling flash devices with FDRProceedings of the 8th International Conference on Frontiers of Information Technology10.1145/1943628.1943646(1-6)Online publication date: 21-Dec-2010
https://dl.acm.org/doi/10.1145/1943628.1943646
Sherif ACavalcanti AJifeng HSampaio A(2010)A process algebraic framework for specification and validation of real-time systemsFormal Aspects of Computing10.1007/s00165-009-0119-622:2(153-191)Online publication date: 1-Mar-2010
https://dl.acm.org/doi/10.1007/s00165-009-0119-6
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents