Article

Empowering the Event-B Method Using External Theories

Authors:

Yamine Aït-Ameur,

Guillaume Dupont,

Dominique Méry,

Peter Rivière,

Neeraj K. SinghAuthors Info & Claims

Integrated Formal Methods: 17th International Conference, IFM 2022, Lugano, Switzerland, June 7–10, 2022, Proceedings

Pages 18 - 35

https://doi.org/10.1007/978-3-031-07727-2_2

Published: 07 June 2022 Publication History

Abstract

Event-B offers a rigorous state-based framework for designing critical systems. Models describe state changes (transitions), and invariant preservation is ensured by inductive proofs over execution traces. In a correct model, such changes transform safe states into safe states, effectively defining a partial function, whose domain prevents ill-defined state changes. Moreover, a state can be formalised as a complex data type, and as such it is accompanied by operators whose correct use is ensured by well-definedness (WD) conditions (partial functions).

This paper proposes to define transitions explicitly as partial functions in an Event-B theory. WD conditions associated to these functions prevent ill-defined transitions in a more effective way than usual Event-B events. We advocate that these WD conditions are sufficient to define transitions that preserve (inductive) invariants and safety properties, thus providing easier and reusable proof methods for model invariant preservation. We rely on the finite automata example to illustrate our approach.

References

[1]

Abrial, J.: The B-book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)

[2]

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

[3]

Abrial, J.R., Butler, M., Hallerstede, S., Leuschel, M., Schmalz, M., Voisin, L.: Proposals for mathematical extensions for Event-B. Technical report (2009). http://deploy-eprints.ecs.soton.ac.uk/216/

[4]

Abrial J-R and Mussat L Bert D, Bowen JP, Henson MC, and Robinson K On using conditional definitions in formal theories ZB 2002:Formal Specification and Development in Z and B 2002 Heidelberg Springer 242-269

[5]

Barringer H, Cheng JH, and Jones CB A logic covering undefinedness in program proofs Acta Inform. 1984 21 251-269

[6]

Bertot Y and Castran P Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions 2010 1 Heidelberg Springer Publishing Company Incorporated

[7]

Börger E and Stärk RF Abstract State Machines. A Method for High-Level System Design and Analysis 2003 Heidelberg Springer

[8]

Butler, M.J., Maamria, I.: Practical theory extension in Event-B. In: Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, pp. 67–81 (2013)

[9]

Dijkstra EW Guarded commands, nondeterminacy and formal derivation of programs Commun. ACM 1975 18 8 453-457

[10]

Dupont G, Aït-Ameur Y, Singh NK, and Pantel M Event-B hybridation: a proof and refinement-based framework for modelling hybrid systems ACM Trans. Embed. Comput. Syst. 2021 20 4 1-37

[11]

Floyd, R.W.: Assigning meanings to programs. In: Proceedings of Symposium in Applied Mathematics - Mathematical Aspects of Computer Science, vol. 19, pp. 19–32 (1967)

[12]

van Gasteren AJM and Tel G Comments on “on the proof of a distributed algorithm”: always-true is not invariant Inf. Process. Lett. 1990 35 6 277-279

[13]

George C Prehn S and Toetenel H The RAISE specification language a tutorial VDM ’91 Formal Software Development Methods 1991 Heidelberg Springer 238-319

[14]

Hoare CAR An axiomatic basis for computer programming Commun. ACM 1969 12 10 576-580

[15]

Jones CB Partial functions and logics: a warning Inf. Process. Lett. 1995 54 2 65-67

[16]

Jones CB and Middelburg CA A typed logic of partial functions reconstructed classically Acta Inform. 1994 31 5 399-430

[17]

Jones, C.B.: Systematic Software Development Using VDM. Prentice Hall International Series in Computer Science, Prentice Hall, Hoboken (1986)

[18]

Lamport L Specifying Systems. The TLA+ Language and Tools for Hardware and Software Engineers 2002 Boston Addison-Wesley

[19]

Leuschel M Dongol B and Troubitsyna E Fast and effective well-definedness checking Integrated Formal Methods 2020 Cham Springer 63-81

[20]

Mendil, I., Singh, N.K., Aït-Ameur, Y., Méry, D., Palanque, P.: An integrated framework for the formal analysis of critical interactive systems. In: Liu, Y., Ma, S.P., Chen, S., Sun, J. (eds.) The 27th Asia-Pacific Software Engineering Conference, June Sun, p. 10. IEEE, Singapore, Singapore, December 2020

[21]

Mendil I, Aït-Ameur Y, Singh NK, Méry D, and Palanque P Qin S, Woodcock J, and Zhang W Leveraging Event-B theories for handling domain knowledge in design models Dependable Software Engineering. Theories, Tools, and Applications 2021 Cham Springer 40-58

[22]

Mendil I, Aït-Ameur Y, Singh NK, Méry D, and Palanque P Lluch Lafuente A and Mavridou A Standard conformance-by-construction with Event-B Formal Methods for Industrial Critical Systems 2021 Cham Springer International Publishing 126-146

[23]

Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL. A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002).

[24]

Owre S, Rushby JM, and Shankar N Kapur D PVS: a prototype verification system Automated Deduction—CADE-11 1992 Heidelberg Springer 748-752

[25]

Riviere P Raschke A and Méry D Formal meta engineering Event-B: extension and reasoning the

E B 4 E B

framework Rigorous State-Based Methods 2021 Cham Springer 153-157

[26]

Spivey, J.M.: Z Notation - A Reference Manual, 2 edn. Prentice Hall International Series in Computer Science, Prentice Hall, Hoboken (1992)

[27]

Stoddart B, Dunne S, and Galloway A Undefined expressions and logic in Z and B Formal Methods Syst. Des. 1999 15 3 201-215

Cited By

Zhang FZhang LZhao YLiu YSun J(2023)Refinement-based Specification and Analysis of Multi-core ARINC 653 Using Event-BFormal Aspects of Computing10.1145/361718335:4(1-29)Online publication date: 21-Nov-2023
https://dl.acm.org/doi/10.1145/3617183
Cervelle JGervais F(2023)Introducing Inductive Construction in B with the Theory PluginRigorous State-Based Methods10.1007/978-3-031-33163-3_4(43-58)Online publication date: 30-May-2023
https://dl.acm.org/doi/10.1007/978-3-031-33163-3_4

Index Terms

Empowering the Event-B Method Using External Theories

Index terms have been assigned to the content through auto-classification.

Recommendations

Towards the Composition of Specifications in Event-B

The development of a system can start with the creation of a specification. Following this viewpoint, we claim that often a specification can be constructed from the combination of specifications which can be seen as composition. Event-B is a formal ...
A method of refinement in UML-B

UML-B is a `UML-like' graphical front-end for Event-B that provides support for object-oriented and state machine modelling concepts, which are not available in Event-B. In particular, UML-B includes class diagram and state machine diagram editors with ...
Semantics Formalisation – From Event-B Contexts to Theories
Rigorous State-Based Methods
Abstract
The Event-B modelling language has been used to formalise the semantics of other modelling languages such as Time Mobility (TiMo) or State Chart XML (SCXML). Typically, the syntactical elements of the languages are captured as Event-B contexts ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Integrated Formal Methods: 17th International Conference, IFM 2022, Lugano, Switzerland, June 7–10, 2022, Proceedings

Jun 2022

371 pages

ISBN:978-3-031-07726-5

DOI:10.1007/978-3-031-07727-2

Editors:
Maurice H. ter Beek
ISTI-CNR, Pisa, Italy
,
Rosemary Monahan
Maynooth University, Maynooth, Ireland

© Springer Nature Switzerland AG 2022.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 07 June 2022

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 27 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Zhang FZhang LZhao YLiu YSun J(2023)Refinement-based Specification and Analysis of Multi-core ARINC 653 Using Event-BFormal Aspects of Computing10.1145/361718335:4(1-29)Online publication date: 21-Nov-2023
https://dl.acm.org/doi/10.1145/3617183
Cervelle JGervais F(2023)Introducing Inductive Construction in B with the Theory PluginRigorous State-Based Methods10.1007/978-3-031-33163-3_4(43-58)Online publication date: 30-May-2023
https://dl.acm.org/doi/10.1007/978-3-031-33163-3_4

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents