Real Time Formal Specification using VDM++
Abstract
VDM++ is a formal Object Oriented Specification language, derived from VDM. It extends VDM by providing object-orientation, real-time as well as parallel features. The use of the language is supported by design guidelines and a tool set. The latter offers graphical representations, syntactic and semantic checking, pretty printing and code generation. In this paper we address the handling of particular real-time issues as supported by the language. An outline specification case study is included.
Keywords:
Software Engineering, Real-time Object-Oriented processing, Transportation
References
Dürr, E (1994), The use of Object-Oriented Specifications in Physics. PhD Thesis, Utrecht University, Utrecht, The Netherlands, 1994, ISBN 90-393-0684-2.
E. Dürr, and N. Plat Editors (1995). VDM++ Language Reference Manual, Afrodite (ESPRIT-III project number 6500) document AFRO/CG/ED.LRM/V10, Cap Volmac, see: http://www.ifad.dk/projects/afrodite
Dürr, E. and J. van Katwijk, (1992), VDM++. A formal Specifications Language for Object-Oriented Designs. In: Georg Heeg, Boris Magnusson, Editors technology of Object-Oriented Languages and Systems, pp 63 - 78. Prentice hall International, Proceedings of Tools Europe '92.
Goldberg, A., Editor, (1984) Smalltalk-80, The Interactive Programming Environment. Addison Wesley Publishing Company.
Jones, C. (1990). Systematic Software Development using VDM (2nd edition). Prentice Hall International.
America, P. (1986) Definition of the programming language POOL-T, Esprit 415 document 0091, Philips Research Laboratories, Eindhoven
Goldsack, S. (1991) Distributed Object Orientation, Journal of Object Oriented Programming, Volume 4, no.1, March/April 1991.
Mahoney, B. and Hayes, I. Using Continuous Real Functions to Model Time Histories, In Bailes, P. Editor, Proceedings of the 6th Australian Software Engineering Conference (ASWECS91), pp 257-270, Australian Computer Society.
B.Mahoney and I.J.Hayes, A case-study in Timed Refinement: A mine Pump, IEEE transactions on Software Engineering, Sept. 1992, pp 817-826
C.Millerchip, B. Mahoney, I.J. Hayes, A Whole System Specification of the Boiler System, in D.Bel Belluz and H.C. Ratz(eds.), "Software Safety: Everybody's business- proc 1993 Int. Workshop on Design and Review of Software Controlled Safety Related Systems", 1994
Eugène Dürr, Stephen Goldsack and Nico Plat. Rigorous Development of Concurrent Object Oriented Systems. Tutorial(MM5) at the Tools Europe 94 Conference, March 7-10,Versailles France. In : Technology of Object Oriented Languages and Systems, Editors. B Magnusson,B.Meyer, J.Nerson, J.F. Perrot TOOLS 13, ISBN 0-13-350539-1, Prentice Hall, UK, (page 515)
Ton Biegstraaten, Klaas Brink, Jan van kstwijk, Hans Toetenel. A simple railroad controller: A case study in real-time specification. Technical Report 94-86. Reports of the Faculty of Technical Mathematics and Informatics. Delft University of Technology, Delft 1994.
------. VDM Specification Language: Proto-Standard(Draft). Document N-246(1-9), BSI IST/5/-/19 and ISO/IEC JTC1/SC22/WG19, December 1992.
Eugène Dürr, N.Plat and Michiel de Boer, Tracking and Tracing Rail Traffic using VDM++: ln M.G.Hinchey and J.P. Bowen Editors : Applications of Formal Methods, Chapter 9, Prentice Hall, September 1995 ISBN 0-13-366949-1.
Concurrent and Real Specifications in VDM++ in : S.Goldsack and S. Kent Editors: Formal Methods in Object Technology Prentice Hall, March 96, ISBN 3-540-19977-2.
J. van Katwijk, W.J. Toetenel. Comparing formal specifications by measuring. Proceedings of the second International Workshop on Real-Time Computing Systems and Applications. TEEE 1995, ISBN 0-8186-7106-8, pp 184 - 190.
G. Bruno et al. A New Petri Net based Formalism for specification, Design and Analysis of Real-Time Systems. In: Proceedings IEEE Real-Time Systems Symposium, IEEE 1993 pp 294-301.
L. Lamport. The Temporal Logic Of Actions. ACM Toplas, 16 (3) 872-923 1995
Y. Kesten, A. Pnueli.Time and hybrid State charts and their textual representation. In: Proceedings 2-nd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. Vol 571 LNCS, pp 591-620 Springer Verlag 1992.
Ghessi G., R. Kemmerer. Astral: an Assertion language for Specifving Real-Time Systemas. Proceedings of the 3-d Europesn Software Engineering Conference 1991, pp 122-146 1991
R. Gerber, Insup Lee. A Layered Approach to Automating the Verification of Real-Time Systema. IEEE Transactions on Software Engineering. Vol 18 no 9, september 1992, pp 768 - 784.
S. Goldsack, K.Lano, E.E.Dürr, Annealing and Datadecomposition VDM** ACM Sigplan Notices, Vol 31, No 7, July 1996
S.Goldsack, K.Lano, E.H.Dirr, Refinement of Object Struetures in VDM**, from ftp://theory.docic.ac.uk, get file at papers/Goldsack/annealing.ps
S. Kent and R. Moore, An Aziomatic Semantics for VDM*? : OO aspecta, Afrodite Document, July 1993, AFRO/IC/SK/SEM-OO/V2
K.Lano Espressing the Semantics of VDM++ in RTL, November 1994, AFRO/1C/KL/SEM2/v2
K.Lano Reasoning techniques in VDM++, November 1994, AFRO/IC/KL/RT/V2
K.Lano, S. Goldsack, J. Bicarregui, S. Kent Real-time Action Logic and Applications, ECOOP 96, Linz Austria, The Proofs workshop, June 6 1996 to appear
Mary Shaw, Comparing Architectural Design Styles in IEEE Software Nov. 1995
E. Dürr, and N. Plat Editors (1995). VDM++ Language Reference Manual, Afrodite (ESPRIT-III project number 6500) document AFRO/CG/ED.LRM/V10, Cap Volmac, see: http://www.ifad.dk/projects/afrodite
Dürr, E. and J. van Katwijk, (1992), VDM++. A formal Specifications Language for Object-Oriented Designs. In: Georg Heeg, Boris Magnusson, Editors technology of Object-Oriented Languages and Systems, pp 63 - 78. Prentice hall International, Proceedings of Tools Europe '92.
Goldberg, A., Editor, (1984) Smalltalk-80, The Interactive Programming Environment. Addison Wesley Publishing Company.
Jones, C. (1990). Systematic Software Development using VDM (2nd edition). Prentice Hall International.
America, P. (1986) Definition of the programming language POOL-T, Esprit 415 document 0091, Philips Research Laboratories, Eindhoven
Goldsack, S. (1991) Distributed Object Orientation, Journal of Object Oriented Programming, Volume 4, no.1, March/April 1991.
Mahoney, B. and Hayes, I. Using Continuous Real Functions to Model Time Histories, In Bailes, P. Editor, Proceedings of the 6th Australian Software Engineering Conference (ASWECS91), pp 257-270, Australian Computer Society.
B.Mahoney and I.J.Hayes, A case-study in Timed Refinement: A mine Pump, IEEE transactions on Software Engineering, Sept. 1992, pp 817-826
C.Millerchip, B. Mahoney, I.J. Hayes, A Whole System Specification of the Boiler System, in D.Bel Belluz and H.C. Ratz(eds.), "Software Safety: Everybody's business- proc 1993 Int. Workshop on Design and Review of Software Controlled Safety Related Systems", 1994
Eugène Dürr, Stephen Goldsack and Nico Plat. Rigorous Development of Concurrent Object Oriented Systems. Tutorial(MM5) at the Tools Europe 94 Conference, March 7-10,Versailles France. In : Technology of Object Oriented Languages and Systems, Editors. B Magnusson,B.Meyer, J.Nerson, J.F. Perrot TOOLS 13, ISBN 0-13-350539-1, Prentice Hall, UK, (page 515)
Ton Biegstraaten, Klaas Brink, Jan van kstwijk, Hans Toetenel. A simple railroad controller: A case study in real-time specification. Technical Report 94-86. Reports of the Faculty of Technical Mathematics and Informatics. Delft University of Technology, Delft 1994.
------. VDM Specification Language: Proto-Standard(Draft). Document N-246(1-9), BSI IST/5/-/19 and ISO/IEC JTC1/SC22/WG19, December 1992.
Eugène Dürr, N.Plat and Michiel de Boer, Tracking and Tracing Rail Traffic using VDM++: ln M.G.Hinchey and J.P. Bowen Editors : Applications of Formal Methods, Chapter 9, Prentice Hall, September 1995 ISBN 0-13-366949-1.
Concurrent and Real Specifications in VDM++ in : S.Goldsack and S. Kent Editors: Formal Methods in Object Technology Prentice Hall, March 96, ISBN 3-540-19977-2.
J. van Katwijk, W.J. Toetenel. Comparing formal specifications by measuring. Proceedings of the second International Workshop on Real-Time Computing Systems and Applications. TEEE 1995, ISBN 0-8186-7106-8, pp 184 - 190.
G. Bruno et al. A New Petri Net based Formalism for specification, Design and Analysis of Real-Time Systems. In: Proceedings IEEE Real-Time Systems Symposium, IEEE 1993 pp 294-301.
L. Lamport. The Temporal Logic Of Actions. ACM Toplas, 16 (3) 872-923 1995
Y. Kesten, A. Pnueli.Time and hybrid State charts and their textual representation. In: Proceedings 2-nd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. Vol 571 LNCS, pp 591-620 Springer Verlag 1992.
Ghessi G., R. Kemmerer. Astral: an Assertion language for Specifving Real-Time Systemas. Proceedings of the 3-d Europesn Software Engineering Conference 1991, pp 122-146 1991
R. Gerber, Insup Lee. A Layered Approach to Automating the Verification of Real-Time Systema. IEEE Transactions on Software Engineering. Vol 18 no 9, september 1992, pp 768 - 784.
S. Goldsack, K.Lano, E.E.Dürr, Annealing and Datadecomposition VDM** ACM Sigplan Notices, Vol 31, No 7, July 1996
S.Goldsack, K.Lano, E.H.Dirr, Refinement of Object Struetures in VDM**, from ftp://theory.docic.ac.uk, get file at papers/Goldsack/annealing.ps
S. Kent and R. Moore, An Aziomatic Semantics for VDM*? : OO aspecta, Afrodite Document, July 1993, AFRO/IC/SK/SEM-OO/V2
K.Lano Espressing the Semantics of VDM++ in RTL, November 1994, AFRO/1C/KL/SEM2/v2
K.Lano Reasoning techniques in VDM++, November 1994, AFRO/IC/KL/RT/V2
K.Lano, S. Goldsack, J. Bicarregui, S. Kent Real-time Action Logic and Applications, ECOOP 96, Linz Austria, The Proofs workshop, June 6 1996 to appear
Mary Shaw, Comparing Architectural Design Styles in IEEE Software Nov. 1995
Published
1996-10-14
How to Cite
DÜRR, Eugène; GOLDSACK, Stephen; KATWIJK, Jan van.
Real Time Formal Specification using VDM++. In: BRAZILIAN SYMPOSIUM ON SOFTWARE ENGINEERING (SBES), 10. , 1996, São Carlos/SP.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
1996
.
p. 57-72.
DOI: https://doi.org/10.5753/sbes.1996.24437.
