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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Notation \(f[X]\) defines a relation image: \(f[X] = \{z \mid y \in X \cap \hbox {dom}(f) \wedge z = f(y)\}\).
- 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.
\(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.
\(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.
Operator is defined as .
References
Iliasov, A., Bryans, J.: Event-B development of Fischer’s algorithm. http://iliasov.org/fischer
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)
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (2005)
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)
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)
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)
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)
Butler, M., Falampin, J.: An approach to modelling and refining timing properties in B. In: Refinement of Critical Systems (RCS), January 2002
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)
Davies, J.: Specification and Proof in Real-time CSP (1993)
Futch, M.J.: Leibniz’s Metaphysics of Time and Space (2008)
Jensen, H.E.: Abstraction-based verification of distributed systems. Technical report, Aalborg University, Department of Computer Science (1999)
Lano, K.: The B Language and Method: A Guide to Practical Formal Development. Springer-Verlag New York, Inc., Secaucus (1996)
Luchangco, V.: Using Simulation Techniques to Prove Timing Properties (1995)
Lynch, N., Vaandrager, F.: Forward and backward simulations - part II: Timing-based systems. Inf. Comput. 128, 1–25 (1996)
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)
RODIN. Event-B Platform (2009). http://www.event-b.org/
de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and Their Comparison (2008)
Schneider, S.: Concurrent and Real Time Systems: The CSP Approach. Wiley, New York (1999)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights 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)