A Framework for Modeling and Analyzing Complex Distributed Systems

This Small Business Technology Transfer Phase II project will develop computational support tools for specifying, analyzing, and verifying designs for complex distributed systems, such as communication systems and transportation control systems. The tools will support a modeling language, called TIOA (Timed Input/Output Automata), developed before and during our Phase I project. The overall modeling and analysis framework will provide an integrated suite of tools and methods for use by customers, leading to qualitative improvements in the design of dependable distributed systems. Building on the Phase I accomplishments, this project will provide: (a) a formal modeling language, TIOA, for specifying timed, asynchronous, and interacting systems components, (b) the front-end processor for TIOA, incorporating syntax and type checking, supporting composition of automata, and providing interfaces to a suite of computer-aided design and analysis tools, (c) a simulation tool allowing simulation of individual specifications and of pairs consisting of a behavior specification and an abstract implementation, (d) an integrated theorem-proving capability through an interface to PVS, and (e)~a model-checking tool. This project will also set the stage for eventual development of tools enabling computer-aided generation of code from TIOA specifications.