Top

Published in:

2023 | OriginalPaper | Chapter

Formalising Liveness Properties in Event-B with the Reflexive EB4EB Framework

Authors : P. Rivière, N. K. Singh, Y. Aït-Ameur, G. Dupont

Published in: NASA Formal Methods

Publisher: Springer Nature Switzerland

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

The correct-by-construction state-based Event-B formal method lacks the ability to express liveness properties using temporal logic. To address this challenge, two approaches can be envisioned. First, embed Event-B models in another formal method supporting liveness properties verification. This method is cumbersome and error-prone, and the verification result is not guaranteed on the source model. Second, extend Event-B to support the expression of and reasoning on liveness properties, and more generally temporal properties. Following the second approach, in [20], J.-R. Abrial and T. S. Hoang proposed an axiomatisation of linear temporal logic (LTL) for Event-B with a set of proof obligations (POs) allowing to verify these properties. These POs are mathematically formalised, but are neither implemented nor generated automatically. In this paper, using the reflexive EB4EB framework [37, 38] allowing for manipulation of the core concepts of Event-B, we propose to formalise and operationalise the automatic generation of proof obligations associated to liveness properties expressed in LTL. Furthermore, relying on trace-based semantics, we demonstrate the soundness of this formalisation, and provide a set of intermediate and generic theorems to increase the rate of proof automation for these properties. Finally, a case study is proposed to demonstrate the use of the defined operators for expressing and proving liveness properties.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter From the Standards to Silicon: Formally Proved Memory Controllers

next chapter Formalized High Level Synthesis with Applications to Cryptographic Hardware

https://www.irit.fr/~Peter.Riviere/models/.

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

Aït Ameur, Y. et al.: Empowering the Event-B method using external theories. In: ter Beek, M.H., Monahan, R. (eds.) Integrated Formal Methods. IFM 2022. LNCS, vol. 13274, pp. 18–35. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-07727-2_2

Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL . In: Bernardo, M., Corradini, F. (eds.) Formal Methods for the Design of Real-Time Systems. SFM-RT 2004. LNCS, vol. 3185. Springer, Berlin, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30080-9_7

Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer Berlin, Heidelberg (2004). https://doi.org/10.1007/978-3-662-07964-5

Bicarregui, J.C., Ritchie, B.: Reasoning about VDM developments using the VDM support tool in mural. In: Prehn, S., Toetenel, W.J. (eds.) VDM 1991. LNCS, vol. 551, pp. 371–388. Springer, Heidelberg (1991). https://doi.org/10.1007/3-540-54834-3_23CrossRef

Bodeveix, J.-P., Filali, M.: Event-B formalization of Event-B contexts. In: Raschke, A., Méry, D. (eds.) ABZ 2021. LNCS, vol. 12709, pp. 66–80. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-77543-8_5CrossRef

Bodeveix, J., Filali, M., Garnacho, M., Spadotti, R., Yang, Z.: Towards a verified transformation from AADL to the formal component-based language FIACRE. Elsevier SCP 106, 30–53 (2015)

Butler, M., et al.: Formal modelling techniques for efficient development of railway control products. In: Fantechi, A., Lecomte, T., Romanovsky, A. (eds.) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. RSSRail 2017. LNCS, vol. 10598, pp. 71–86. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68499-4_5

Butler, M., et al.: The first twenty-five years of industrial use of the B-Method. In: ter Beek, M.H., Ničković, D. (eds.) FMICS 2020. LNCS, vol. 12327, pp. 189–209. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-58298-2_8CrossRef

10.

Butler, M., Maamria, I.: Practical theory extension in Event-B. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 67–81. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39698-4_5CrossRef

11.

Castéran, P.: An explicit semantics for event-b refinements. In: Ait-Ameur, Y., Nakajima, S., Méry, D. (eds.) Implicit and Explicit Semantics Integration in Proof-Based Developments of Discrete Systems, pp. 155–173. Springer, Singapore (2021). https://doi.org/10.1007/978-981-15-5054-6_8CrossRef

12.

Cimatti, A., et al.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45657-0_29CrossRef

13.

Dupont, G., Aït Ameur, Y., Singh, N.K., Pantel, M.: Event-B hybridation: a proof and refinement-based framework for modelling hybrid systems. ACM TECS 20(4), 35:1–35:37 (2021)

14.

Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de Moura, L.: A metaprogramming framework for formal verification. ACM PACMPL 1(ICFP), 34:1–34:29 (2017)

15.

Fallenstein, B., Kumar, R.: Proof-producing reflection for HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 170–186. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22102-1_11CrossRef

16.

Farrell, M., Monahan, R., Power, J.F.: An institution for Event-B. In: James, P., Roggenbach, M. (eds.) WADT 2016. LNCS, vol. 10644, pp. 104–119. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-72044-9_8CrossRef

17.

Farrell, M., Monahan, R., Power, J.F.: Building specifications in the Event-B institution. Log.Methods Comput. Sci. 18(4) (2022). https://doi.org/10.46298/lmcs-18(4:4)2022

18.

Halchin, A., Ameur, Y.A., Singh, N.K., Ordioni, J., Feliachi, A.: Handling B models in the PERF integrated verification framework: formalised and certified embedding. Sci. Comput. Program. Elsevier 196, 102477 (2020)CrossRef

19.

Hallerstede, S., Hoang, T.S.: Refinement of decomposed models by interface instantiation. Elsevier SCP 94, 144–163 (2014)

20.

Hoang, T.S., Abrial, J.-R.: Reasoning about liveness properties in Event-B. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 456–471. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24559-6_31CrossRef

21.

Hoang, T.S., Schneider, S., Treharne, H., Williams, D.M.: Foundations for using linear temporal logic in Event-B refinement. Formal Aspects Comput. 28(6), 909–935 (2016). https://doi.org/10.1007/s00165-016-0376-0MathSciNetCrossRefMATH

22.

Holzmann, G.: Spin Model Checker, The: Primer and Reference Manual, first edn. Addison-Wesley Professional, Boston (2003)

23.

Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47CrossRef

24.

Lamport, L.: Proving the correctness of multiprocess programs. IEEE TSE 3(2), 125–143 (1977)MathSciNetMATH

25.

Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston (2002)

26.

Leroy, X., Blazy, S., Kästner, D., Schommer, B., Pister, M., Ferdinand, C.: CompCert - a formally verified optimizing compiler. In: Embedded Real Time Software and Systems (ERTS). SEE (2016)

27.

Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. Springer Int. J. STTT 10(2), 185–203 (2008)

28.

Manna, Z., Pnueli, A.: Adequate proof principles for invariance and liveness properties of concurrent programs. Elsevier SCP 4(3), 257–289 (1984)MathSciNetMATH

29.

Mendil, I., Riviere, P., Ameur, Y.A., Singh, N.K., Méry, D., Palanque, P.A.: Non-intrusive annotation-based domain-specific analysis to certify event-b models behaviours. In: 29th Asia-Pacific Software Engineering Conference, APSEC, pp. 129–138. IEEE (2022)

30.

Méry, D., Poppleton, M.: Towards an integrated formal method for verification of liveness properties in distributed systems: with application to population protocols. SoSyM 16(4), 1083–1115 (2017)

31.

Mitra, S., Archer, M.: PVS strategies for proving abstraction properties of automata. In: International Workshop on Strategies in Automated Deduction. ENTCS, vol. 125, pp. 45–65. Elsevier (2004)

32.

Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9

33.

Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55602-8_217CrossRef

34.

Paul van der Walt: Reflection in Agda. Master’s thesis, University of Utrecht, Department of Computing Science (2012)

35.

Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 151–166. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0054170CrossRef

36.

Riccobene, E., Scandurra, P.: Towards an interchange language for ASMs. In: Zimmermann, W., Thalheim, B. (eds.) ASM 2004. LNCS, vol. 3052, pp. 111–126. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24773-9_9CrossRef

37.

Riviere, P., Singh, N.K., Aït Ameur, Y.: EB4EB: a framework for reflexive Event-B. In: International Conference on Engineering of Complex Computer Systems, ICECCS 2022, pp. 71–80. IEEE (2022)

38.

Riviere, P., Singh, N.K., Aït Ameur, Y.: Reflexive Event-B: semantics and correctness the EB4EB framework. IEEE Transactions on Reliability, pp. 1–16 (2022)

39.

Riviere, P., Singh, N.K., Aït Ameur, Y., Dupont, G.: Standalone Event-B models analysis relying on the EB4EB meta-theory. In: Glässer, U., Campos, J.C., Méry, D., Palanque, P. (eds.) International Conference on Rigorous State Based Methods, ABZ 2023. LNCS, vol. 14010. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-33163-3_15

40.

Singh, N.K.: Using Event-B for Critical Device Software Systems. Springer, London (2013). https://doi.org/10.1007/978-1-4471-5260-6

41.

Sozeau, M., et al.: The MetaCoq project. Springer J. Autom. Reason. 64(5), 947–999 (2020)MathSciNetCrossRef

42.

Su, W., Abrial, J.: Aircraft landing gear system: approaches with Event-B to the modeling of an industrial system. Springer Int. J. STTT 19(2), 141–166 (2017)

43.

Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_59CrossRef

44.

Zhu, C., Butler, M., Cirstea, C., Hoang, T.S.: A fairness-based refinement strategy to transform liveness properties in Event-B models. Elsevier SCP 225, 102907 (2023)

Title: Formalising Liveness Properties in Event-B with the Reflexive EB4EB Framework
Authors: P. Rivière
N. K. Singh
Y. Aït-Ameur
G. Dupont
Publisher: Springer Nature Switzerland
Book: NASA Formal Methods
Print ISBN: 978-3-031-33169-5

Electronic ISBN: 978-3-031-33170-1

Copyright Year: 2023
DOI: https://doi.org/10.1007/978-3-031-33170-1_19

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner