Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Engineering Methods

ICFEM 2011: Formal Methods and Software Engineering pp 179–194Cite as

A Deterministic Interpreter Simulating a Distributed Real Time System Using VDM

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6991))

Abstract

The real time dialect of VDM, called VDM-RT, contains constructs for describing concurrent threads, synchronisation of such threads and the distribution of object instances and their threads over multiple CPUs with busses connecting them. Tools that simulate an executable subset of VDM-RT models benefit from being deterministic so that problems are reproducible and can be more easily investigated. We describe the deterministic scheduling features of our VDM-RT interpreter, and show how multi-threaded models can also be debugged deterministically.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Babaoglu, Ö., Marzullo, K.: Consistent Global States of Distributed Systems: Fundamental Concepts and Mechanisms. Tech. Rep. UBLCS-93-1, University of Bologna, Piazza di Porta S. Donato, 5, 40127 Bologna (Italy) (January 1993)

    Google Scholar 

  2. Battle, N.: VDMJ User Guide. Tech. rep., Fujitsu Services Ltd., UK (2009)

    Google Scholar 

  3. Bergan, T., Anderson, O., Devietti, J., Ceze, L., Grossman, D.: CoreDet: A Compiler and Runtime System for Deterministic Multithreaded Execution. In: ASPLOS 2010. ACM, New York (2010)

    Google Scholar 

  4. Bjorner, D., Jones, C.B. (eds.): The Vienna Development Method: The Meta-Language. LNCS, vol. 61. Springer, Heidelberg (1978)

    MATH  Google Scholar 

  5. Breuer, P., Bowen, J.: Towards correct executable semantics for z. In: Bowen, J., Hall, J. (eds.) Z User Workshop, pp. 185–209. Springer, Heidelberg (1994)

    Google Scholar 

  6. Burdy, L., Cheon, Y., Cok, D., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML Tools and Applications. Intl. Journal of Software Tools for Technology Transfer 7, 212–232 (2005)

    Article  Google Scholar 

  7. Burnin, J., Sen, K.: Asserting and checking determinism for multithreaded programs. In: 17th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE). ACM, New York (2009)

    Google Scholar 

  8. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L. (eds.): All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  9. Dick, A., Krause, P., Cozens, J.: Computer aided transformation of Z into Prolog. In: Nicholls, J. (ed.) Z User Workshop, Workshops in Computing, pp. 71–85. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  10. Fitzgerald, J.S.: The Typed Logic of Partial Functions and the Vienna Development Method. In: Bjørner, D., Henson, M.C. (eds.) Logics of Specification Languages. EATCS Monographs in Theoretical Computer Science, pp. 427–461. Springer, Heidelberg (2007)

    Google Scholar 

  11. Fitzgerald, J.S., Larsen, P.G., Verhoef, M.: Vienna Development Method. Wiley Encyclopedia of Computer Science and Engineering. John Wiley & Sons, Inc., Chichester (2008)

    Book  Google Scholar 

  12. Fitzgerald, J., Larsen, P.G.: Modelling Systems – Practical Tools and Techniques in Software Development, 2nd edn. Cambridge University Press, Cambridge (2009); ISBN 0-521-62348-0

    Book  MATH  Google Scholar 

  13. Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs for Object–oriented Systems. Springer, New York (2005), http://www.vdmbook.com

    MATH  Google Scholar 

  14. Fitzgerald, J., Larsen, P.G., Sahara, S.: VDMTools: Advances in Support for Formal Modeling in VDM. ACM Sigplan Notices 43(2), 3–11 (2008)

    Article  Google Scholar 

  15. Florescu, O., Voeten, J., Verhoef, M., Corporaal, H.: Reusing Real-Time Systems Design Experience Through Modelling Patterns. In: Forum on specification and Description Languages (FDL). ECSI (2006); received the best paper award at FDL 2006. This paper is available on-line at, http://www.es.ele.tue.nl/premadona/publications/FVVC06.pdf

  16. Fröhlich, B.: Towards Executability of Implicit Definitions. Ph.D. thesis, TU Graz, Institute of Software Technology (September 1998)

    Google Scholar 

  17. Hooman, J., Verhoef, M.: Formal semantics of a VDM extension for distributed embedded systems. In: Dams, D., Hannemann, U., Steffen, M. (eds.) Concurrency, Compositionality, and Correctness. LNCS, vol. 5930, pp. 142–161. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  18. Jones, C.B.: Program Specification and Verification in VDM. Logic of Programming and Calculi of Discrete Design F36, 149–184 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  19. Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall International, Englewood Cliffs (1990); ISBN 0-13-880733-7

    MATH  Google Scholar 

  20. Kneuper, R.: Symbolic Execution as a Tool for Validation of Specifications. Ph.D. thesis, Department of Computer Science, Univeristy of Manchester (March 1989), technical Report Series UMCS-89-7-1

    Google Scholar 

  21. Lamport, L.: Time, Clocks, and the Ordering of Events in a Distributed System. Communications of the ACM 21(7), 558–565 (1978)

    Article  MATH  Google Scholar 

  22. Larsen, P.G.: Evaluation of underdetermined explicit expressions. In: Naftalin, M., Bertrán, M., Denvir, T. (eds.) FME 1994. LNCS, vol. 873, pp. 233–250. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  23. Larsen, P.G., Battle, N., Ferreira, M., Fitzgerald, J., Lausdahl, K., Verhoef, M.: The Overture Initiative – Integrating Tools for VDM. ACM Software Engineering Notes 35(1) (January 2010)

    Google Scholar 

  24. Larsen, P.G., Lassen, P.B.: An Executable Subset of Meta-IV with Loose Specification. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol. 551, Springer, Heidelberg (1991)

    Google Scholar 

  25. Larsen, P.G., Lausdahl, K., Battle, N.: The VDM-10 Language Manual. Tech. Rep. TR-2010-06, The Overture Open Source Initiative (April 2010)

    Google Scholar 

  26. Larsen, P.G., Pawłowski, W.: The Formal Semantics of ISO VDM-SL. Computer Standards and Interfaces 17(5-6), 585–602 (1995)

    Article  Google Scholar 

  27. Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185–203 (2008)

    Article  Google Scholar 

  28. McCarthy, J.: A Basis for a Mathematical Theory of Computation. In: Braffort, P., Hirstberg, D. (eds.) Western Joint Computer Conference, then published in: Computer Programming and Formal Systems, pp. 33–70. North Holland, Amsterdam (1967)

    Google Scholar 

  29. Microsystems, S.: Java Debug Wire Protocol. 1.5.0 edn. Sun Microsystems, Inc, (2004), http://download.oracle.com/javase/1.5.0/docs/guide/jpda/jdwp-spec.html

  30. Plagge, D., Leuschel, M.: Validating Z Specifications Using the ProB Animator and Model Checker. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 480–500. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  31. Plat, N., Larsen, P.G.: An Overview of the ISO/VDM-SL Standard. Sigplan Notices 27(8), 76–82 (1992)

    Article  Google Scholar 

  32. Rethans, S.C.A.D.: A Common Debugger Protocol for Languages and Debugger UI Communication. XDEBUG, 2 edn. (2011), http://www.xdebug.org/docs-dbgp.php

  33. Ribeiro, A., Larsen, P.G.: Proof obligation generation and discharging for recursive definitions in VDM. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 40–55. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  34. Rushby, J.: Formal Methods: Instruments of Justification or Tools for Discovery? In: Nordic Seminar on Dependable Computing System 1994. The Technical University of Denmark, Department of Computer Science (August 1994)

    Google Scholar 

  35. Rushby, J.: Disappearing formal methods. In: Fifth IEEE International Symposium on High Assurance Systems Engineering, HASE 2000. IEEE, Los Alamitos (2000)

    Google Scholar 

  36. Sherrell, L.B., Carver, D.L.: Experiences in Translating Z Designs to Haskell Implementations. Software Practice and Experience 24(12), 1159–1178 (1994)

    Article  Google Scholar 

  37. Søndergaard, H., Sestoft, P.: Non-determinism in Functional Languages. The Computer Journal 35(5), 514–523 (1992)

    Article  MathSciNet  Google Scholar 

  38. Theelen, B., Florescu, O., Geilen, M., Huang, J., van der Putten, P., Voeten, J.: Software/hardware engineering with the parallel object-oriented specification language. In: Proceedings of the ACM-IEEE International Conference on Formal Methods and Models for Codeesign (MEMOCODE), pp. 139–148. IEEE Computer Society, Los Alamitos (2007)

    Google Scholar 

  39. Valentine, S.: Z− −, an executable subset of Z. In: Nicholls, J. (ed.) Z User Workshop, Workshops in Computing, pp. 157–187. Springer, Heidelberg (1992)

    Google Scholar 

  40. Verhoef, M.: Modeling and Validating Distributed Embedded Real-Time Control Systems. Ph.D. thesis, Radboud University Nijmegen (2008); ISBN 978-90-9023705-3

    Google Scholar 

  41. Verhoef, M., Larsen, P.G., Hooman, J.: Modeling and Validating Distributed Embedded Real-Time Systems with VDM++. In: Misra, J., Nipkow, T., Karakostas, G. (eds.) FM 2006. LNCS, vol. 4085, pp. 147–162. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  42. Woodcock, J.C.P., Cavalcanti, A.L.C.: A concurrent language for refinement. In: Butterfield, A., Pahl, C. (eds.) IWFM 2001: 5th Irish Workshop in Formal Methods. BCS Electronic Workshops in Computing, Dublin, Ireland (July 2001)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Aarhus School of Engineering, Dalgas Avenue 2, DK-8000, Aarhus C, Denmark

    Kenneth Lausdahl & Peter Gorm Larsen

  2. Fujitsu Services, Lovelace Road, Bracknell, Berkshire, RG12 8SN, UK

    Nick Battle

Authors
  1. Kenneth Lausdahl
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Peter Gorm Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Nick Battle
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing, Teesside University, UK

    Shengchao Qin

  2. LMAM and Department of Informatics, School of Mathematical Sciences,, Peking University, China

    Zongyan Qiu

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lausdahl, K., Larsen, P.G., Battle, N. (2011). A Deterministic Interpreter Simulating a Distributed Real Time System Using VDM. In: Qin, S., Qiu, Z. (eds) Formal Methods and Software Engineering. ICFEM 2011. Lecture Notes in Computer Science, vol 6991. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24559-6_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-24559-6_14

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-24558-9

  • Online ISBN: 978-3-642-24559-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation