An Extensible and Scalable Framework for Formal Modeling, Analysis, and Development of Distributed Systems

This STTR Phase I project has the goal of substantially advancing the state of the art in constructing software for complex distributed systems, including Internet communication protocols; protocols for communication and computation in mobile ad hoc networks; robot and transportation control systems; and security protocols. The proposed multi-pronged approach includes defining formal languages that can be used to represent distributed systems and their components; developing theory and methodology to provide a sound mathematical basis for modeling systems and reasoning about their properties; designing and building scalable analysis tools that can be used to formally specify distributed systems, timed systems, and hybrid/probabilistic systems, assist in the validation of correctness and performance properties; and designing and building automated synthesis tools that can generate executable code from system models and produce efficient deployment schemes of the software components in target networks. The distributed executable code will provably preserve the properties of the abstract specifications. The computer-aided design tools will be integrated within an extensible and scalable architecture, and offer a flexible and easy to use integrated development environment for the framework's users. Our overall framework will build on and extend the Input/Output Automata (IOA) and Timed Input/Output Automata (TIOA) frameworks developed in our prior research.