Abstract
This paper presents work performed in the EPSRC “Object-oriented Specification of Reactive and Real-time Systems” project. It aims to provide formal design methods for real-time systems, using a combination of the VDM++ formal method and the HRT-HOOD method.
We identify refinement steps for hard real-time systems in VDM++, together with a case study of a mine-pump control system, involving a combination of VDM++ and HRT-HOOD.
We also consider the representation of hybrid systems in VDM++.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M Awad, J Kuusela, and Jurgen Ziegler. Object-oriented Technology for Real-time Systems. Prentice Hall, 1996.
P I Barton, E Smith and C C Pantelides. Combined Discrete/Continuous Process Modelling Using gPROMS, 1991 AIChE Annual Meeting: Recent Advances in Process Control, Los Angeles, 1991.
P Barton and T Park. Analysis and Control of Combined Discrete/Continuous Systems: Progress and Challenges in the Chemical Processing Industries, in proceedings of Chemical Process Control — V: Assessment and New Directions for Research, January, 1996.
A Burns and A Wellings. HRT-HOOD: A structured design method for hard real-time systems. Real-Time Systems, 6(1):73–114, January 1994.
D Coleman, P Arnold, S Bodoff, C Dollin, H Gilchrist, F Hayes, and P Jeremaes. Object-oriented Development: The FUSION Method. Prentice Hall Object-oriented Series, 1994.
S Cook and J Daniels. Designing Object Systems: Object-Oriented Modelling with Syntropy. Prentice Hall, Sept 1994.
E Durr, S Goldsack, and J van Katjwick. Specification of a cruise controller in VDM++. In Proceedings of Real Time OO Workshop, ECOOP 96, 1996.
S M Celiktin. Interval-Based Techniques for the Specification and Analysis of Real-Time Requirements, PhD thesis, Catholic University of Louvain, September 1994.
S Engell and S Kowalewski. Discrete Events and Hybrid Systems in Process Control, Proceedings of Chemical Process Control — V: Assessment and New Directions for Research, January, 1996.
J Fiadeiro and T Maibaum. Describing, Structuring and Implementing Objects, in de Bakker et al., Foundations of Object Oriented languages, LNCS 489, Springer-Verlag, 1991.
F Jahanian and A K Mok. Safety Analysis of Timing Properties in Real-time Systems, IEEE Transactions on Software Engineering, SE-12, pp. 890–904, September 1986.
S Kent and K Lano. Axiomatic Semantics for Concurrent Object Systems, AFRODITE Technical Report AFRO/IC/SKKL/SEM/V1, Dept. of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ.
K Lano. Distributed System Specification in VDM ++, FORTE '95 Proceedings, Chapman and Hall, 1995.
K Lano, J Bicarregui and S Kent. A Real-time Action Logic of Objects, ECOOP 96 Workshop on Proof Theory of Object-oriented Systems, Linz, Austria, 1996.
K Lano. Semantics of Real-Time Action Logic, Technical Report GR/K68783-3, Dept. of Computing, Imperial College, 1996.
K Lano, S Goldsack and A Sanchez. Transforming Continuous into Discrete Specifications with VDM ++, IEE C8 Colloquium Digest on Hybrid Control for real-time Systems, 1996.
K Lano. Refinement and Simulation of Real-time and Hybrid Systems using VDM ++ and gPROMS, ROOS project report GR/K68783-13, November 1996, Dept. of Computing, Imperial College.
G Lowe and H Zedan. Refinement of complex systems: A case study. The Computer Journal, 38(10):785–800, 1995.
Z Manna and A Pnueli. Time for concurrency. Technical report, Dept. of Computer Science, Stanford University, 1992.
B Mahony and I J Hayes. Using continuous real functions to model timed histories. In P A Bailes, editor, Proceedings of 6th Australian Software Engineering Conference. Australian Computer Society, July 1991.
J S Ostroff. Temporal Logic for Real-Time Systems. John Wiley, 1989.
A Pnueli. Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. In J de Bakker, W P de Roever, and G Rozenberg, editors, Current Trends in Concurrency, LNCS vol. 224, Springer-Verlag, 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lano, K., Goldsack, S., Bicarregui, J. (1997). Integrating VDM++ and real-time system design. In: Bowen, J.P., Hinchey, M.G., Till, D. (eds) ZUM '97: The Z Formal Specification Notation. ZUM 1997. Lecture Notes in Computer Science, vol 1212. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027290
Download citation
DOI: https://doi.org/10.1007/BFb0027290
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62717-3
Online ISBN: 978-3-540-68490-9
eBook Packages: Springer Book Archive