Extending the Power and Applicability of the Timed Input/Output Automata Framework

这个项目正在推进为复杂的分布式系统构建软件的技术水平，包括Internet通信协议等例子；移动AD hoc网络中的通信与计算协议机器人和运输控制系统；还有安全协议。本项目所采用的方法使分布式系统的严格派生成为可能，而这些系统以前只能以一种特别的方式指定，不可避免地导致无法保证遵守功能和行为需求的实现。该项目开发了一个全面的计算机支持框架，基于健全的数学原理，用于复杂系统的建模、分析和生成代码。在这个项目中开发的整体框架建立并扩展了成功的定时和非定时输入/输出自动机（IOA）框架。本研究项目包括以下技术领域：(1)开发语言和相关建模和分析理论，扩展IOA和定时IOA，支持定时、混合和概率输入/输出自动机及其组合。这些为表达现代分布式系统的特性提供了全面的便利。(2)开发工具，支持使用我们的新语言表达的分布式系统设计分析。(3)开发工具和支持理论，用于根据规范自动和计算机辅助生成分布式代码，并支持推导从软件组件到物理网络节点的正确和优化的映射。(4)利用该理论开发了几个复杂的应用程序，既解决了应用领域中的重要问题，又证明了形式化框架的有效性。

This project is advancing the state of the art in constructing software for complex distributed systems, including such examples as Internet communication protocols; protocols for communication and computation in mobile ad hoc networks; robot and transportation control systems; and security protocols. The approach pursued in this project enables rigorous derivations of distributed systems that previously could be specified only in an ad hoc way, invariably leading to implementations whose adherence to functional and behavioral requirements could not be guaranteed. This project develops a comprehensive computer-supported framework, based on sound mathematical principles, for modeling, analyzing, and generating code for complex systems.The overall framework developed in this projects builds on and extends the successful timed and untimed Input/Output Automata (IOA) frameworks. This research project envelopes the following technical areas: (1) Developing languages and associated modeling and analysis theory, extending IOA and Timed IOA, and supporting timed, hybrid, and probabilistic Input/Output Automata, and combinations thereof. These provide comprehensive facilities for expressing properties of modern distributed systems. (2) Developing tools supporting analysis of distributed system designs expressed using our new languages. (3) Developing tools and supporting theory for automated and computer-aided generation of distributed code from specifications, and supporting the derivation of correct and optimized mappings from software components to physical network nodes. (4) Developing several sophisticated applications using the theory, both solving important problems in their application domains and demonstrating the effectiveness of the formal framework.