Abstract
We are interested in specifying and verifying dynamic properties of reactive systems with the B method extended with propositional linear temporal logic PLTL. Commonly, specification of dynamic properties is done with pure future fragment of PLTL. However, the introduction of past operators enables the production of more natural formulation of a wide class of dynamic properties. In this paper, we show how the past fragment of PLTL, as well as the future fragment is preserved by the B refinement, and we present patterns of reformulation and the corresponding sufficient conditions to verify dynamic properties including past time operators by means of cooperation of theorem proving and model checking.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.R.: The B Book. Cambridge University Press, Cambridge (1996)
Abrial, J.R.: Extending B without changing it (for developing distributed systems). In: Habrias, H. (ed.) Proc. of the 1-st Conference on the B method, Putting into Practice Methods and Tools for Information System Design, Nantes, France, pp. 169–190 (1996)
Abrial, J.R., Mussat, L.: Introducing dynamic constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 83–128. Springer, Heidelberg (1998)
Benedetti, M., Cimatti, A.: Bounded Model Checking for Past LTL. TACAS, 18–33 (2003)
Bellegarde, F., Darlot, C., Julliand, J., Kouchnarenko, O.: Reformulation: a way to combine dynamic properties and B refinement. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 2–19. Springer, Heidelberg (2001)
Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: 17MV: a new Symbolic Model Verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)
Darlot, C.: Reformulation et Vérification de propriétés temporelles dans le cadre du raffinement de systèmes d’événements, Phd thesis, Université de Franche – Comté (2002)
Darlot, C., Julliand, J., Kouchnarenko, O.: Refinement Preserves PLTL Properties. In: Bert, D., P. Bowen, J., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 408–420. Springer, Heidelberg (2003)
Emerson, E.A.: Temporel and modal logic. Handbook of Theoretical computer scienc, vol. B. Elsevier Science Publisher. B.V, Amsterdam (1990)
Gabbay, D.: The declarative past and imperative future. In: Barringer, H. (ed.) Proceedings of the Colloquium on Temporal Logic and Specifications. LNCS, vol. 398, pp. 409–448. Springer, Heidelberg (1989)
Julliand, J., Masson, P.-A., Mountassir, M.: Modular verification of dynamic properties for reactive systems. In: Proc. of the 1-st Int. Workshop on Integrated Formal Methods (IFM 1999), pp. 89–108. Springer, Heidelberg (1999)
Julliand, J., Masson, P.-A., Mountassir, H.: Vérification par model Checking modulaire des propriétés dynamiques introduites en B. TSI 20(7) (2001)
Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Parikh, R. (ed.) Proceedings of the Conference on Logic of Programs. Lecture Note in Computer Science, vol. 193, pp. 196–218. Springer, Heidelberg (1985)
Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal Logic with Forgettable Past. In: 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 383–392. Soc. Press, Copenhagen (2002)
Manna, Z., Pnuelli, A.: The Temporal Logic of Reactive and Concurrent Systems Specification. Springer, Heidelberg (1992)
Markey, N.: Past is for free: on the complexity of verifying linear temporal properties with past. In: Proc. 9th Int. Workshop on Expressiveness in Concurrenc (EXPRESS 2002), Brno, Czech Republic. Electronic Notes in Theorie of Computer Science, vol. 68(2). Elsevier Science, Amsterdam (2002)
Pnueli, A.: The temporal semantics of concurrent programs. Theoretical Computer Science 13, 45–60 (1981)
Saad, M., Jemni Ben Ayed, L.: A way to Introduce Dynamic Properties with Past Temporal Operators in the B Refinement. Accepted as poster in the international ACM/IEEE conference MEMOCODE 2004 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Saad, M., Ayed, L.J.B. (2005). Introducing Dynamic Properties with Past Temporal Operators in the B Refinement. In: Peled, D.A., Tsay, YK. (eds) Automated Technology for Verification and Analysis. ATVA 2005. Lecture Notes in Computer Science, vol 3707. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11562948_24
Download citation
DOI: https://doi.org/10.1007/11562948_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29209-8
Online ISBN: 978-3-540-31969-6
eBook Packages: Computer ScienceComputer Science (R0)