ITR: A Framework for Rapid Development of Reliable Robotics Software

ITR：快速开发可靠机器人软件的框架

• 批准号: 0205542
• 负责人: Paul Hudak
• 金额: $ 51.03万
• 依托单位: Yale University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2002
• 资助国家: 美国
• 起止时间: 2002-09-01 至 2006-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0205542&HistoricalAwards=false
• 关键词: ITR; Framework; Rapid; Development; Reliable

Taha, WalidCCR-0205542"ITR: A Framework for Rapid Development of Reliable Robotics Software"Robots are entering daily life. Commercially available systems aredelivering medication to patients in hospitals, mowing lawns, vacuumingfloors, and finding wide applications in the entertainment industry. In the future, they will play a more substantial role in areas such as space exploration, health care, and search and rescue. But asthese applications grow, so does the complexity of these robots, makingthe reliability of their software and the productivity of theirprogrammers a priority. It is not clear that current techniques forprogramming robots are sufficient for building systems that are orders of magnitude more complex than the ones available today. The vast majority of programming methods in current use focus on high-level planning and task and behavioral aspects. By contrast, there are no widely-accepted specialized software processes or programming languages for the integrated development of robotics applications.This project explores the impact of state-of-the-art programming languages techniques in a small-scale robotics setting. The project applies domain-specific languages methods and automatic program generation techniques. The framework exploits core technologies such as multi-stage programming with simple, high-level annotationsto avoid unnecessary runtime overheads yet provide a natural and algorithmic approach to program generation, where generation occurs in a first stage, and the execution of the synthesized program occurs in a second stage. Because (even when the final goal is embedded software) the first stage does not need to be resource-bounded, conventional programming techniques can be used. The challenge, then, becomes ensuring that the generated programs are suitable for execution on an embedded platform. Multi-stage languages already provide significant safety guarantees. For example, a program generator written in such a language not only is type-safe in the traditional sense, but we are guaranteed that any generated program will also be type safe. This provides a noteworthy degree of assurance about the quality of the generated code. But like most traditional high-level programming techniques, multi-stage programming was designed to satisfy functional requirements rather than operational ones, and existing multi-stage languages do not provide any guarantees about the behavior of programs in the presence of bounded resources. The focus of this project is ways to address this problem by strengthening``traditional'' multi-stage type systems using a number of state-of-the-art techniques from type theory and functional reactive programming (FRP) to create resource-aware multi-stage programming. Linear and alias types (in conjunction with dependent typing) will be used to ensure space-boundedness, new typing techniques are used to ensure time-boundedness, and signals and behaviors from FRP allow for a natural style of reactive programming.

Taha，WalidCCR-0205542“ITR：快速开发可靠机器人软件的框架“机器人正在进入日常生活。 商业上可用的系统正在为医院的病人提供药物，修剪草坪，吸尘地板，并在娱乐业中找到广泛的应用。 未来，他们将在太空探索、医疗、搜救等领域发挥更大的作用。 但随着这些应用的增长，这些机器人的复杂性也在增加，这使得软件的可靠性和程序员的生产力成为优先考虑的问题。目前尚不清楚，目前的机器人编程技术是否足以构建比今天可用的系统复杂数量级的系统。 目前使用的绝大多数编程方法都集中在高级规划以及任务和行为方面。 相比之下，没有广泛接受的专门的软件流程或编程语言的机器人应用程序的集成开发。本项目探讨了国家的最先进的编程语言技术在小规模的机器人设置的影响。 该项目应用领域特定语言方法和自动程序生成技术。 该框架利用核心技术，如多阶段编程与简单的，高层次的annotationto避免不必要的运行时开销，但提供了一个自然的和算法的方法来生成程序，其中生成发生在第一阶段，和执行的合成程序发生在第二阶段。因为（即使最终目标是嵌入式软件）第一阶段不需要资源受限，可以使用传统的编程技术。挑战，然后，成为确保生成的程序是适合于在嵌入式平台上执行。多阶段语言已经提供了重要的安全保证。例如，用这种语言编写的程序生成器不仅在传统意义上是类型安全的，而且可以保证任何生成的程序也是类型安全的。 这为生成的代码的质量提供了值得注意的保证。 但是像大多数传统的高级编程技术一样，多阶段编程被设计为满足功能需求而不是操作需求，并且现有的多阶段语言不提供关于存在有限资源的程序行为的任何保证。 这个项目的重点是如何解决这个问题，通过加强“传统”的多阶段类型系统，使用一些国家的最先进的技术，从类型理论和功能反应式编程（FRP），以创建资源意识的多阶段编程。线性和别名类型（结合依赖类型）将用于确保空间有界性，新的类型技术用于确保时间有界性，来自FRP的信号和行为允许自然风格的反应式编程。