Declarative networks are specified using Network Datalog (NDlog), a distributed logic-based recursive query language. DNV is a integrated framework for design, implementation, and verification of declarative network. The initial verification cases in this page utilize a standard formal verification technique called interactive theorem proving. DNV provides a framework to bridge network design, formal verification, and implementation, as depicted in the right picture.
Interactive theorem provers built on higher-order logic are extremely expressive and flexible. PVS and Coq are two standard/popular proof assistants. While Coq is based on "Calculus of Inductive Constructions" which makes it particularly useful to reason about recursive objects, PVS is equipped with a CTL model checker, a ground evaluator, and animation/testing support which makes it an integrated system to explore many state-of-art formal technique. PVS and Coq are therefore particularly useful for our initial explore in applying DNV to the recursive tuples manipulated by declarative network.
Both PVS and Coq allow definition, reasoning about functions or predicates, mathematical theorems, and software specifications. Proof steps are carried out interactively in a goal-directed manner, where user supplies high-level proof command to guide the proof assistant to complete the rest of th proof.
DNV takes as input: (1) declarative networking specification written in NDlog, which is automatically mapped into logical axioms in the form of PVS/Coq codes; and invariants/properties; and (2) invariants/properties to be checked in the form of either NDlog specification or PVS/Coq codes. The verification is then completed in PVS/Coq directed by user-supplied proof-scripts.
We provide several examples below with both the NDlog input (NDlog source files), and PVS codes + proof scripts (PVS dump files).
To re-play the verification, inside PVS, open the PVS dump file, and invoke M-x undump-pvs-files and M-x prove-pvs-file. More details on using PVS.