Skip to main content
SpringerLink
Log in

A Proof-Based Method for Modelling Timed Systems

  • Conference paper
  • First Online:
Perspectives of System Informatics (PSI 2014)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8974))

Abstract

We present a novel method for reasoning about time in state-based proof-oriented formalisms. The method builds on a non-classical model of time, the Leibnizian model, in which time is a relative property determined by the observations of an evolving subject, rather than one of the fundamental dimensions. It proves to be remarkably effective in the context of the Event-B formalism. We illustrate the method with a machine-checked proof of Fischer’s algorithm that, to our knowledge, is simpler than other proofs available in the literature.

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

Access this chapter

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 EPUB and 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

Institutional subscriptions

Notes

  1. 1.

    Notation \(f[X]\) defines a relation image: \(f[X] = \{z \mid y \in X \cap \hbox {dom}(f) \wedge z = f(y)\}\).

  2. 2.

    \(f;g\) is a forward relational composition: \(f;g = \{ a\mapsto b \mid a \mapsto e \in f \wedge e \mapsto b \in g\}\).

  3. 3.

    \(d_H(A, B) = \max \{ \sup _{x \in A} \inf _{y \in B} d(x, y), \sup _{x \in B} \inf _{y \in A} d(x, y) \}\).

  4. 4.

    \(a\,\Vert \,b = \{ (x \mapsto i) \mapsto (y \mapsto j) \mid x \mapsto y \in a \wedge i \mapsto j \in b\}\) (parallel product).

  5. 5.

    Operator is defined as .

References

  1. Iliasov, A., Bryans, J.: Event-B development of Fischer’s algorithm. http://iliasov.org/fischer

  2. Abadi, M., Lamport, L.: An old-fashioned recipe for real time. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 1–27. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  3. Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (2005)

    Google Scholar 

  4. Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)

    Book  Google Scholar 

  5. Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  6. Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: Météor: a successful application of B in a large project. In: Wing, J.M., Woodcock, J. (eds.) FM 1999. LNCS, vol. 1708, p. 369. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  7. Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: Uppaal - a tool suite for automatic verification of real-time systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  8. Butler, M., Falampin, J.: An approach to modelling and refining timing properties in B. In: Refinement of Critical Systems (RCS), January 2002

    Google Scholar 

  9. Cansell, D., Méry, D., Rehm, J.: Time constraint patterns for event B development. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 140–154. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  10. Davies, J.: Specification and Proof in Real-time CSP (1993)

    Google Scholar 

  11. Futch, M.J.: Leibniz’s Metaphysics of Time and Space (2008)

    Google Scholar 

  12. Jensen, H.E.: Abstraction-based verification of distributed systems. Technical report, Aalborg University, Department of Computer Science (1999)

    Google Scholar 

  13. Lano, K.: The B Language and Method: A Guide to Practical Formal Development. Springer-Verlag New York, Inc., Secaucus (1996)

    Book  Google Scholar 

  14. Luchangco, V.: Using Simulation Techniques to Prove Timing Properties (1995)

    Google Scholar 

  15. Lynch, N., Vaandrager, F.: Forward and backward simulations - part II: Timing-based systems. Inf. Comput. 128, 1–25 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  16. Moller, F., Tofts, C.: A temporal calculus of communicating systems. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 401–415. Springer, Heidelberg (1990)

    Google Scholar 

  17. RODIN. Event-B Platform (2009). http://www.event-b.org/

  18. de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and Their Comparison (2008)

    Google Scholar 

  19. Schneider, S.: Concurrent and Real Time Systems: The CSP Approach. Wiley, New York (1999)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Newcastle University, Newcastle, UK

    Alexei Iliasov & Jeremy Bryans

Authors
  1. Alexei Iliasov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jeremy Bryans
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alexei Iliasov .

Editor information

Editors and Affiliations

  1. School of Computer Science, University of Manchester, Manchester, United Kingdom

    Andrei Voronkov

  2. A.P. Ershov Institute of Informatics Systems, Novosibirsk, Russia

    Irina Virbitskaite

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Iliasov, A., Bryans, J. (2015). A Proof-Based Method for Modelling Timed Systems. In: Voronkov, A., Virbitskaite, I. (eds) Perspectives of System Informatics. PSI 2014. Lecture Notes in Computer Science(), vol 8974. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46823-4_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-46823-4_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-46822-7

  • Online ISBN: 978-3-662-46823-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation