Towards An Integrated Formal Method for Verification of Liveness Properties in Distributed Systems: with application to Population Protocols

Dominique Méry 1, 2, 3, 4 Mike Poppleton 5
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
4 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
5 School of Electronics and Computer Science
ECS - School of Electronics and Computer Science
Abstract : State-based Formal Methods (e.g Event-B/RODIN \cite{Abr:10,ABH:10}) for critical system development and verification are now well-established, with track records including tool support and industrial applications. The focus of proof-based verification in particular, is on safety properties. Liveness properties, which guarantee {\em eventual}, or converging computations of some requirements, are less well dealt with. Inductive reasoning about liveness is not explicitly supported. Liveness proofs are often complex and expensive, requiring high skill levels on the part of the verification engineer. Fairness-based temporal logic approaches have been proposed to address this, e.g. TLA \cite{lamport94a} and that of Manna \& Pnueli~\cite{DBLP:books/daglib/0080029}. We contribute to this technology need by proposing a fairness-based method integrating temporal and first order logic, proof and tools for modelling and verification of safety and liveness properties. The method is based on an integration of Event-B and TLA. Building on our previous work~\cite{MP:13}, we present the method via three example population protocols \cite{AAD:06}. These were proposed as a theoretical framework for computability reasoning about Wireless Sensor Network (WSN) and Mobile Ad-Hoc Network (MANET) algorithms. Our examples present typical liveness and convergence requirements. We prove convergence results for the examples by integrated modelling and proof with Event-B/RODIN and TLA. We exploit existing proof rules, define and apply three new proof rules; soundness proofs are also provided. During the process we observe certain repeating patterns in the proofs. These are easily identified and reused because of the explicit nature of the reasoning.
Liste complète des métadonnées

https://hal.inria.fr/hal-01245819
Contributeur : Dominique Méry <>
Soumis le : jeudi 17 décembre 2015 - 16:43:20
Dernière modification le : mercredi 22 novembre 2017 - 11:02:25

Identifiants

  • HAL Id : hal-01245819, version 1

Collections

Citation

Dominique Méry, Mike Poppleton. Towards An Integrated Formal Method for Verification of Liveness Properties in Distributed Systems: with application to Population Protocols. Software and Systems Modeling (SoSyM), Springer, 2015. 〈hal-01245819〉

Partager

Métriques

Consultations de la notice

190