Input/Output Automata (IOA) is an expressive specification framework with built-in properties for compositional reasoning. It has been shown to be effective in specifying and analyzing distributed and networked systems. The available verification engines for IOA are based on interactive theorem provers such as Isabelle, Larch, PVS, and Coq, and are expressive but require heavy human interaction. Motivated by the advances in SMT solvers, in this work we explore a different expressivity-automation tradeoff for IOA. We present Dione, the first IOA analysis system built with dafny and its SMT-powered toolchain and demonstrate its effectiveness on four distributed applications. Our translator tool converts Python-esque Dione language specification of IOA and their properties to parameterized Dafny modules. Dione automatically generates the relevant compatibility and composition lemmas for the IOA specifications,which can then be checked with Dafny on a per module-basis. We ensure that all resulting formulas are expressed mostly in fragments solvable by SMT solvers and hence enables Bounded Model Checking and k-induction-based invariant checking using Z3. We present successful applications of DIONE in verification of an asynchronous leader election algorithm, two self-stabilizing mutual exclusion algorithms, and CAN bus Arbitration. We automatically prove key invariants of all four protocols; for the last three this involves reasoning about arbitrary number of participants. These analyses are largely automatic with minimal manual inputs needed, and they demonstrate the effectiveness of this approach in analyzing networked and distributed systems.
展开▼
