Project Website http://groups.csail.mit.edu/tds/formal.html
A major effort of the Theory of Distributed Systems (TDS) Group is the development of formal models and methods for describing and reasoning about distributed and real-time systems. The models we favor are based on mathematical objects such as state machines, rather than being tied to any specific programming language, specification language or proof logic. Indeed, our models are flexible enough to support many different languages and proof methods.
We begin with general-purpose models and methods and build special-purpose, application-specific models and methods upon them. Our models support composable system design and verification, with many resulting benefits (reliability, reusability, maintainability, etc.). Specifications for system building blocks may include not only safety and liveness properties, but also more complex properties involving performance, reliability, probability and continuous behavior.
The general-purpose modelling begins with our work on the I/O automaton model, a labelled transition system model for components in asynchronous concurrent systems. It continues with our work on the timed automaton model, a similar model for components in real-time systems. Other work incorporates liveness, probability, and continuous behavior . Proof methods supported include assertional and simulation methods, process algebraic methods, and temporal logic methods. We have also developed structure for carrying out computer-aided verification of systems based on I/O automata and timed automata, using the Larch Prover.
The special-purpose modelling involves building formal frameworks for particular application areas. See our work on applications. Such a framework consists of a body of abstract component descriptions, abstract algorithms, verification methods and theorems designed to support the particular application.