Advertisement

A Proof-Based Method for Modelling Timed Systems

  • Alexei Iliasov
  • Jeremy Bryans
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, 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.

Keywords

Critical Section Mutual Exclusion Proof Obligation Simulation Relation Observer Model 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Iliasov, A., Bryans, J.: Event-B development of Fischer’s algorithm. http://iliasov.org/fischer
  2. 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) CrossRefGoogle Scholar
  3. 3.
    Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (2005)Google Scholar
  4. 4.
    Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)CrossRefGoogle Scholar
  5. 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) CrossRefGoogle Scholar
  6. 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) CrossRefGoogle Scholar
  7. 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) CrossRefGoogle Scholar
  8. 8.
    Butler, M., Falampin, J.: An approach to modelling and refining timing properties in B. In: Refinement of Critical Systems (RCS), January 2002Google Scholar
  9. 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) CrossRefGoogle Scholar
  10. 10.
    Davies, J.: Specification and Proof in Real-time CSP (1993)Google Scholar
  11. 11.
    Futch, M.J.: Leibniz’s Metaphysics of Time and Space (2008)Google Scholar
  12. 12.
    Jensen, H.E.: Abstraction-based verification of distributed systems. Technical report, Aalborg University, Department of Computer Science (1999)Google Scholar
  13. 13.
    Lano, K.: The B Language and Method: A Guide to Practical Formal Development. Springer-Verlag New York, Inc., Secaucus (1996) CrossRefGoogle Scholar
  14. 14.
    Luchangco, V.: Using Simulation Techniques to Prove Timing Properties (1995)Google Scholar
  15. 15.
    Lynch, N., Vaandrager, F.: Forward and backward simulations - part II: Timing-based systems. Inf. Comput. 128, 1–25 (1996)CrossRefMATHMathSciNetGoogle Scholar
  16. 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. 17.
    RODIN. Event-B Platform (2009). http://www.event-b.org/
  18. 18.
    de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and Their Comparison (2008)Google Scholar
  19. 19.
    Schneider, S.: Concurrent and Real Time Systems: The CSP Approach. Wiley, New York (1999)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  1. 1.Newcastle UniversityNewcastleUK

Personalised recommendations