Framework for Modeling and Analyzing Complex Distributed Systems

摘要

Report developed under STTR contract for topic AF04-T023. This Phase I project developed a modeling language and laid a foundation for computational support tools for specifying, analyzing, and verifying complex distributed system designs. Ultimately, the overall modeling and analysis framework will provide an integrated suite of tools and methods leading to qualitative improvements in the design of dependable distributed systems. In more detail, this project developed: (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. This project provides the basis for refining the language and extending and integrating the associated tool set in Phase II.