Nothing Special   »   [go: up one dir, main page]

Skip to main content

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

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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

Similar content being viewed by others

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

Authors

Corresponding author

Correspondence to Alexei Iliasov .

Editor information

Editors and Affiliations

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