FMitF: Track I: Automating the Verification of Distributed Systems

Regents Of The University Of Michigan - Ann Arbor, Ann Arbor MI

Investigators

Abstract

Computer software is and has always been teeming with errors. When these errors manifest in a deployed system they can cause severe problems, including undesired behavior and unavailability of critical services. Formal verification is an approach that allows the writing of software that is provably free of such errors, but is notoriously difficult and time-consuming, which makes it harder to adopt in practice. The proposed research will investigate a new approach for automating the verification of complex software running on multiple machines, thus bringing formal verification closer to becoming a practical reality. This proposal will automate the verification process by automatically identifying inductive invariants. It uses model checking to identify an inductive invariant of a small, finite instance of the system and then tries to generalize that invariant to all possible instances. The proposed work is structured along three thrusts. The first thrust will expand this initial idea to cover invariants with existential quantifiers, thus broadening the scope of the approach. The second thrust will scale the approach to more complicated systems by adding support for refinement. The third thrust will go beyond decidable verification in order to support high-performance implementations. The proposed work’s broader impact is multi-faceted. First, it represents a path for bringing formal verification closer to practical use and ensuring it does not remain just an academic exercise. This will further enable building and deploying stable and reliable systems to the immediate benefit of all end users. On the academic side, this project aims to debunk the common belief that model checking is not applicable to complex distributed systems due to its limited scalability. By doing so, this project will bring together theorem proving and model checking, two areas that have long been walking parallel paths towards correctness. The data generated through this work (specifications, implementations, proofs, configurations and script files) will be retained in a secure machine cluster administered by the research groups of the principal investigators, with electronic data backup service provided by the Departmental Computing Organization of the Electrical Engineering and Computer Science Department at Michigan and the Information and Technology Services of the University of Michigan. They will also be hosted on publicly available repository providers like github.com. Data will be retained for at least three years beyond the award period, as required by NSF guidelines. The current repository can be found at: https://github.com/GLaDOS-Michigan/I4. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.