nach oben

Erschienen in:

2023 | OriginalPaper | Buchkapitel

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

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

Erschienen in: NASA Formal Methods

Verlag: Springer Nature Switzerland

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel From the Standards to Silicon: Formally Proved Memory Controllers

Nächstes Kapitel 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)

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

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

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

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner