A Theorem Proving Approach Towards Declarative Networking
Anduo Wang, Boon Thau Loo, Changbin Liu, Oleg V. Sokolsky, Prithwish Basu · ScholarlyCommons (University of Pennsylvania) · 2009
Abstract. We present the DRIVER system for designing, analyzing and implementing network protocols. DRIVER leverages declarative networking, a recent innovation that enables network protocols to be concisely specified and implemented using declarative languages. DRIVER takes as input declarative networking specifications written in the Network Datalog (NDlog) query language, and maps that automatically into logical specifications that can be directly used in existing theorem provers to validate protocol correctness. As an alternative approach, network designer can supply a component-based model of their routing design, automatically generate PVS specifications for verification and subsequent compilation into verified declarative network implementations. We demonstrate the use of DRIVER for synthesizing and verifying a variety of well-known network routing protocols. 1