Verifiable hierarchical protocols with network invariants on parametric systems

Conference Paper

We present Neo, a framework for designing pre-verified protocol components that can be instantiated and connected in an arbitrarily large hierarchy (tree), with a guarantee that the whole system satisfies a given safety property. We employ the idea of network invariants to handle correctness for arbitrary depths in the hierarchy. Orthogonally, we leverage a parameterized model checker (Cubicle) to allow for a parametric number of children at each internal node of the tree. We believe this is the first time these two distinct dimensions of configuration have been together tackled in a verification approach, and also the first time a proof of an observational preorder (as required by network invariants) has been formulated inside a parametric model checker. Aside from the natural up/down communication between a child and a parent, we allow for peer-to-peer communication, since many real protocol optimizations rely on this paradigm. The paper details the Neo theory, which is built upon the Input-Output Automata formalism, and demonstrates the approach on an example hierarchical cache coherence protocol.

Full Text

Duke Authors

Cited Authors

  • Matthews, O; Bingham, J; Sorin, DJ

Published Date

  • March 24, 2017

Published In

  • Proceedings of the 16th Conference on Formal Methods in Computer Aided Design, Fmcad 2016

Start / End Page

  • 101 - 108

International Standard Book Number 13 (ISBN-13)

  • 9780983567868

Digital Object Identifier (DOI)

  • 10.1109/FMCAD.2016.7886667

Citation Source

  • Scopus