Dione: A Protocol Verification System Built with Dafny for I/O Automata

Chiao Hsieh, Sayan Mitra

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationIntegrated Formal Methods - 15th International Conference, IFM 2019, Proceedings
EditorsWolfgang Ahrendt, Silvia Lizeth Tapia Tarifa
PublisherSpringer
Pages227-245
Number of pages19
ISBN (Print)9783030349677
DOIs
StatePublished - Jan 1 2019
Event15th International Conference on Integrated Formal Methods, IFM 2019 - Bergen, Norway
Duration: Dec 2 2019Dec 6 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11918 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference15th International Conference on Integrated Formal Methods, IFM 2019
CountryNorway
CityBergen
Period12/2/1912/6/19

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Dione: A Protocol Verification System Built with Dafny for I/O Automata'. Together they form a unique fingerprint.

  • Cite this

    Hsieh, C., & Mitra, S. (2019). Dione: A Protocol Verification System Built with Dafny for I/O Automata. In W. Ahrendt, & S. L. Tapia Tarifa (Eds.), Integrated Formal Methods - 15th International Conference, IFM 2019, Proceedings (pp. 227-245). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11918 LNCS). Springer. https://doi.org/10.1007/978-3-030-34968-4_13