Towards an integrated formal method for verification of liveness properties in distributed systems: with application to population protocols

摘要

Statebased formal methods [e.g. Event-B/RODIN (Abrial in Modeling in EventBsystem and software engineering. Cambridge University Press, Cambridge, 2010; Abrial et al. in Int J Softw Tools Technol Transf (STTT) 12(6): 447466, 2010)] for critical system development and verification are now well established, with track records including tool support and industrial applications. The focus of proofbased verification, in particular, is on safety properties. Liveness properties, which guarantee 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 highskill levels on the part of the verification engineer. Fairnessbased temporal logic approaches have been proposed to address this, e.g. TLA Lamport (ACM Trans Program Lang Syst 16(3): 872923, 1994) and that of Manna and Pnueli (Temporal verification of reactive systemssafety. Springer, New York, 1995). We contribute to this technology need by proposing a fairness-based method integrating temporal and firstorder logic, proof and tools for modelling and verification of safety and liveness properties. The method is based on an integration of EventB and TLA. Building on our previous work (Mery and Poppleton in Integrated formal methods, 10th international conference, IFM 2013, Turku, Finland, pp 208-222, 2013. doi: 10.1007/978-3-642-38613-8_15), we present the method via three example population protocols Angluin et al. (Distrib Comput 18(4): 235-253, 2006). These were proposed as a theoretical framework for computability reasoning about Wireless Sensor Network and Mobile Ad-Hoc Network 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.