A Framework for Modeling and Analyzing Complex Distributed Systems

Summary and intellectual merit. This Small Business Technology Transfer Phase I project will develop a modeling language and computational support tools for specifying, analyzing, and verifying complex distributed system designs. The overall modeling and analysis framework will provide an integrated suite of tools and methods ultimately leading to qualitative improvements in the design of dependable distributed systems. In more detail, building on the existing expertise this project will develop: (a) a formal modeling language, called TIOA (Timed Input/Output Automata), for specifying timed, asynchronous, and interacting systems components, (b) the front-end processor for TIOA, incorporating syntax and type checking, and providing interfaces to computer-aided design tools, (c) a simulation tool allowing simulation of specifications and paired simulations of a specification and an abstract implementation, and (d) a theorem-proving link through an interface to PVS. To demonstrate the feasibility of this approach, this project will produce complete examples of specification and analysis of distributed algorithms using this framework. This project will set the stage for extending the language and its front end in Phase II, for integration with model-checking tools, and eventually for development of tools enabling computer-aided generation of code from TIOA specifications.