Extending the Power and Applicability of the Timed Input/Output Automata Framework

Massachusetts Institute Of Technology, Cambridge MA

Investigators

Abstract

This project is advancing the state of the art in constructing software for complex distributed systems, including such examples as Internet communication protocols; protocols for communication and computation in mobile ad hoc networks; robot and transportation control systems; and security protocols. The approach pursued in this project enables rigorous derivations of distributed systems that previously could be specified only in an ad hoc way, invariably leading to implementations whose adherence to functional and behavioral requirements could not be guaranteed. This project develops a comprehensive computer-supported framework, based on sound mathematical principles, for modeling, analyzing, and generating code for complex systems. The overall framework developed in this projects builds on and extends the successful timed and untimed Input/Output Automata (IOA) frameworks. This research project envelopes the following technical areas: (1) Developing languages and associated modeling and analysis theory, extending IOA and Timed IOA, and supporting timed, hybrid, and probabilistic Input/Output Automata, and combinations thereof. These provide comprehensive facilities for expressing properties of modern distributed systems. (2) Developing tools supporting analysis of distributed system designs expressed using our new languages. (3) Developing tools and supporting theory for automated and computer-aided generation of distributed code from specifications, and supporting the derivation of correct and optimized mappings from software components to physical network nodes. (4) Developing several sophisticated applications using the theory, both solving important problems in their application domains and demonstrating the effectiveness of the formal framework.