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