Automated Formal Analysis of Distributed Systems

Anduo Wang
Postdoctoral Research Associate
University of Illinois at Urbana-Champaign
Location: 
SERC 306
Date: 
Friday, April 24, 2015 - 14:00
The past twenty years have witnessed significant advances in formal modeling, system verification and testing of network protocols. However a long-standing challenge in these approaches is the decoupling of a formal reasoning process and the actual distributed implementation.  This talk presents my work on bridging formal reasoning and actual implementation in various distributed systems. First, in the context of Internet routing systems, I will present the Formally Safe Routing (FSR) toolkit, that combines the use of
declarative networking, routing algebra, and SMT solver techniques, in order to synthesize faithful distributed routing implementations from verified network models. I will also describe our work on scaling up the FSR toolkit on Internet-scale configurations. Our core technique uses a configuration rewriting calculus for transforming large network configurations into smaller instances, while preserving routing behaviors. Next, in the context of the emerging software-defined networks, I will present our reactive synthesis approach for rigorous and scalable management of network controllers. Finally, I will conclude with a discussion of my ongoing and future work, on using database techniques for orchestrating software-defined network applications.