Synthesizing Architectural Models of Cyber-Physical Systems
Abstract:
Many formal methods techniques have been developed that help designers build complex, dependable systems. At one extreme, we have interactive theorem proving, which places few restrictions on the kinds of systems and properties that can be verified, but which requires well trained professionals with a deep understanding of logic and proof. At the other extreme, we have methods that find certain classes of errors in a fully automated way, but which place severe restrictions on the kinds of systems and properties they can analyze. Is it possible to have the best of both worlds? Is it possible to have a powerful, expressive modeling language with a powerful deductive engine that can be used to interactively prove theorems and that can be used to automatically generate counterexamples? We show how to do just that with an algorithm that makes essential use of interactive theorem proving technology but analyzes specifications in a fully automated way. Our algorithm allows us to turn an interactive theorem prover into an extensible, automatic, analysis tool that can be used by regular engineers to provide increased assurance in the correctness of their designs. The user is responsible only for modeling and specifying the properties of their design; they are not responsible for providing proofs. It is in this regard that our approach is automatic. Our approach is extensible because it can exploit any existing or newly developed libraries of definitions, theorems and proof techniques. For example, the use of libraries for reasoning about non-linear arithmetic, set theory, the theory of lists, etc., can lead to significant improvements in our ability to prove theorems and to generate counterexamples. The main idea of our algorithm is to use the deductive verification engine of an interactive theorem prover to semantically decompose properties into sub-goals that are either shown to be true or that can be tested to find counterexamples. Deduction and testing proceed in an interleaved, synergistic fashion. We have implemented our algorithm in the ACL2 Sedan (ACL2s), a freely available, open-source, well-supported theorem prover that uses ACL2 as its core reasoning engine. ACL2s is an Eclipse plug-in that provides a modern integrated development environment designed to bring computer-aided reasoning to the masses. ACL2s has been used in several sections of a required freshman course at Northeastern University to teach several hundred undergraduate students how to reason about programs. We will report on our experiences, which include a case study on hardware verification, a comparison with Alloy on a collection of examples from the literature, and our experiences with the use of ACL2s by freshmen students to debug their programs and specifications.
Biography:
I am an Associate Professor in the College of Computer and Information Science at Northeastern University. I received my Ph.D. in Computer Sciences at the University of Texas at Austin in 2001.
My main research interest is mechanized formal verification and validation of computing systems. What guides my research is the vision that formal methods can be used to revolutionize the design and implementation of highly reliable, robust, and scalable systems in a variety of important application areas, ranging from large component-based software systems to hardware systems to aerospace systems to computational biology to public health. My other areas of interest include programming languages, distributed computing, logic, software engineering, algorithms, computer architecture, aerospace, and pedagogy.
Slide presentation will be available for download May 2012.