Formally Verifiable Networking.
Anduo Wang, Limin Jia, Changbin Liu, Boon Thau Loo, Oleg V. Sokolsky, Prithwish Basu · ScholarlyCommons (University of Pennsylvania) · 2009
... (FVN), a novel approach towards unifying the design, specification, implementation, and verification of networking protocols within a logic-based framework. In FVN, formal logical statements are used to specify the behavior and the properties of the protocol. FVN uses declarative networking as an intermediary layer between high-level logical specifications of the network model and low-level implementations. A theorem prover is used to statically verify the properties of declarative network protocols. Moreover, a property preserving translation exists for generating declarative networking implementations from verified formal specifications. We further demonstrate the possibility of designing and specifying well-behaved network protocols with correctness guarantees in FVN using meta-models in a systematic and compositional way.