Decomposing Large, Complex, Concurrent Systems into Manageable Building Blocks

摘要

This project produced many techniques to assist developers in decomposing large, complex, concurrent systems into manageable building blocks. (1) Foundations: A new mathematical modeling framework was developed for hybrid (discrete/continuous) systems. Also, new methods for using small finite-state abstractions in verifying complex distributed algorithms were developed. (2) Distributed systems (2a) Compositional modeling and analysis methods were utilized in the design of several services for group-oriented computation in fault-prone distributed networks. In particular, group communication services supporting a changing set of participating clients, and a group membership service suitable for WANs, were designed and developed. The methods were also used to validate (and find an error in) the Ensemble group communication system. (2b) Substantial progress was made on a mathematical framework for analyzing weakly coherent multiprocessor memories and the programs that use them. (2c) The modeling and analysis methods were also used to develop a new weakly coherent (eventually serializable) data service for distributed networks, and to analyze standard communication protocols, security protocols, and operating systems. (3) Automated transportation systems: The new hybrid system modeling framework was applied to the task of analyzing the behavior of automated multi-vehicle transportation systems. This work included analysis of both ground and air transportation systems. (4) Programming language development: The IOA specification and programming language was defined. A high-level design was produced for a toolset including validation and code generation tools, and substantial progress was made on detailed design and implementation of the toolset.