Skip to Main content Skip to Navigation
Conference papers

Verification by Construction of Distributed Algorithms

Dominique Méry 1, 2, 3, 4
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
4 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : The verification of distributed algorithms is a challenge for formal techniques supported by tools, as model checkers and proof as- sistants. The difficulties, even for powerful tools, lie in the derivation of proofs of required properties, such as safety and eventuality, for dis- tributed algorithms. Verification by construction can be achieved by us- ing a formal framework in which models are constructed at different levels of abstraction; each level of abstraction is refined by the one below, and this refinement relationships is documented by an abstraction relation namely a gluing invariant. The highest levels of abstraction are used to express the required behavior in terms of the problem domain and the lowest level of abstraction corresponds to an implementation from which an efficient implementation can be derived automatically. In this paper, we describe a methodology based on the general concept of refinement and used for developing distributed algorithms satisfying a given list of safety and liveness properties. The modelling methodology is defined in the Event-B modelling language using the IDE Rodin.
Complete list of metadatas

https://hal.inria.fr/hal-02400379
Contributor : Dominique Méry <>
Submitted on : Monday, December 9, 2019 - 2:40:16 PM
Last modification on : Tuesday, December 17, 2019 - 3:04:05 PM

Identifiers

Collections

Citation

Dominique Méry. Verification by Construction of Distributed Algorithms. Theoretical Aspects of Computing - 2019 - 16th International Colloquium, Oct 2019, Mammamet, Tunisia. pp.22-38, ⟨10.1007/978-3-030-32505-3_2⟩. ⟨hal-02400379⟩

Share

Metrics

Record views

44