Abstract
Timed Communicating Object Z (TCOZ) combines Object-Z's strengths in modeling complex data and algorithms with Timed CSP's strengths in modeling real-time concurrency. TCOZ inherits CSP's channel-based communication mechanism, in which messages represent discrete synchronisations between processes. The purpose of most control systems is to observe and control analog components. In such cases, the interface between the control system and the controlled systems cannot be satisfactorily described using the channel mechanism. In order to address this problem, TCOZ is extended with continuousfunction interface mechanisms inspired by process control theory, the sensor and the actuator. The utility of these new mechanisms is demonstrated through their application to the design of an automobile cruise control system.
Acknowledgements
We would like to thank Neale Fulton, Ian Hayes and anonymous referees for many useful comments. This work is supported in part by the DSTO/CSIRO Fellowship programme.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
K. Araki, A. Galloway, and K. Taguchi, editors. IFM’99: Integrated Formal Methods, York,UK. Springer-Verlag, June 1999.
J. Davies. Specification and Proof in Real-Time Systems. PhD thesis, Oxford University Computing Laboratory, Programming Research Group, 1991.
J.S. Dong and B. Mahony. Active Objects in TCOZ. In J. Staples, M. Hinchey, and S. Liu, editors, the 2nd IEEE International Conference on Formal Engineering Methods (ICFEM’98), pages 16–25. IEEE Press, December 1998.
R. Duke, G. Rose, and G. Smith. Object-Z: a Specification Language Advocated for the Description of Standards. Computer Standards and Interfaces, 17:511–533, 1995.
C. J. Fidge, I. J. Hayes, A. P. Martin, and A. K. Wabenhorst. A set-theoretic model for real-time specification and reasoning. In Mathematics of Program Construction, 1998.
C. Fischer. CSP-OZ: A combination of Object-Z and CSP. In H. Bowmann and J. Derrick, editors, Formal Methods for Open Object-Based Distributed Systems (FMOODS’ 97), volume 2, pages 423–438. Chapman & Hall, 1997.
A. J. Galloway and W. J. Stoddart. An operational semantics for ZCCS. In M. Hinchey and S. Liu, editors, the IEEE International Conference on Formal Engineering Methods (ICFEM’97), pages 272–282,Hiroshima, Japan,November 1997. IEEE Press.
I. J. Hayes and B. P. Mahony. Using units of measurement in formal specifications. Formal Aspects of Computing, 7(3), 1995.
I. J. Hayes and M. Utting. Coercing real-time refinement: A transmitter. In D. J. Duke and A. S. Evans, editors, BCS-FACS Northern Formal Methods Workshop,Electronic Workshops in Computing. Springer Verlag, 1997.
B. Mahony and J.S. Dong. Overview of the semantics of TCOZ. InAraki et al. [1].
B. P. Mahony. The Specification and Refinement of Timed Processes. PhD thesis, University of Queensland, 1991.
B. P. Mahony and J.S. Dong. Blending Object-Z and Timed CSP: An introduction to TCOZ. In K. Futatsugi, R. Kemmerer, and K. Torii, editors, The 20th International Conference on Software Engineering (ICSE’98), pages 95–104, Kyoto, Japan, April 1998. IEEE Press.
B. P. Mahony and J.S. Dong. Network topology and a case-study in TCOZ. In ZUM’98 The 11 th International Conference of Z Users. Springer-Verlag, September 1998.
B. P. Mahony and I. J. Hayes. A case-study in timed refinement: A mine pump. IEEE Transactions on Software Engineering, 18(9):817–826, 1992.
F. H. Raven. Automatic Control Engineering. McGraw-Hill, second edition, 1968.
S. Schneider and J. Davies. A brief history of Timed CSP. Theoretical Computer Science, 138, 1995.
M. Shaw. Beyond objects. ACM Software Engineering Notes, 20(1), January 1995.
A. Simpson, J. Davies, and J. Woodcock. Security management via Z and CSP. In J. Grundy, M. Schwenke, and T. Vickers, editors, IRW/FMP’98. Springer-Verlag, 1998.
G. Smith. A semantic integration of Object-Z and CSP for the specification of concurrent systems. In J. Fitzgerald, C. Jones, and P. Lucas, editors, Proceedings of FME’97: IndustrialBenefit of Formal Methods, Graz, Austria, September 1997. Springer-Verlag.
J. M. Spivey. Understanding Z: A Specification Language and its Formal Semantics, Cambridge University Press, 1988.
C. Suhl. RT-Z: An integration of Z and timed CSP. In Araki et al. [1].
K. Taguchi and K. Araki. The State-BasedCCS Semantics for Concurrent Z Specification. In M. Hinchey and S. Liu, editors, the IEEE International Conference on Formal Engineering Methods (ICFEM’97), pages 283–292,Hiroshima, Japan,November 1997. IEEE Press.
P. Zave and M. Jackson. Four dark corners of requirements engineering. ACM Trans. Software Engineering and Methodology, 6(1):1–30, January 1997.
C. Zhou, C. A. R. Hoare, and A. P. Ravn. A calculus of durations. Information Processing Letters, 40:269–276, 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mahony, B., Dong, J.S. (1999). Sensors and actuators in TCOZ. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_12
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive