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

扩展定时输入/输出自动机框架的功能和适用性

• 批准号: 0702670
• 负责人: Nancy Lynch
• 金额: $ 46万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2007
• 资助国家: 美国
• 起止时间: 2007-06-01 至 2012-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0702670&HistoricalAwards=false
• 关键词: Extending; Power; Applicability; Timed; Input

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.

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