Warren A. Hunt, Jr. and Sandip Ray Department of Computer Sciences University of Texas at Austin
{hunt,sandip}@cs.utexas.edu
Reactive concurrent systems, such as routers, consist of a number of interacting processes that perform non-terminating computations while receiving and transmitting messages. The design of such routing systems is error-prone, and non-determinism inherent in concurrent communications makes it hard to detect or diagnose such errors. Our effort will develop ACL2-based tools for ensuring trustworthy execution of large-scale reactive routing systems.
We aim to develop a scalable, mechanized infrastructure for certifying correct and secure execution of reactive routing system implementations through: a generic framework for modeling and specifying systems at a number of abstraction layers; a compositional methodology for mathematically analyzing such models; and developing a suite of tools and techniques to mechanize and automate such analysis within a unified logical foundation. Our research exploits ACL2's general-purpose reasoning engine while augmenting the tool suite with a streamlined modeling and specification methodology. We will develop a collection of targeted tools for verifying safety, liveness, and security properties of such systems while staying within a single logic and proof system.
To facilitate verification of correspondence between protocol layers, we propose to enhance ACL2's reasoning engine with automated verification tools based on advances in BDD- and SAT-based techniques. The invention and proof of inductive invariants is one of the most time-consuming activities in reactive system verification, and we will integrate into ACL2 a general-purpose symbolic simulation capability; this technique can symbolically simulate system models over a large number of computation steps, thereby often obviating the construction of single-step inductive invariants. The expected results will help automate the mechanical verification of reactive systems such as routers and CPSs.
