ITR: A Framework for Rapid Development of Reliable Robotics Software

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

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.