Formal Modelling and Verification

A major effort of the 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. Our 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. Our 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. Models Task-PIOAs and Security Verification I/O Automata Timed Automata Probabilistic Automata Hybrid Automata Tools IOA Language and Toolset Other Computer-Aided Verification Liveness Applications

TOC / LCS / MIT Last modified: August 27, 1999	Comments?