Rigorous automated implementation of dependable distributed real-time systems (RAIDR)

实时分布式多核系统的设计和实现往往涉及到许多微妙的细节，这是因为它们固有的复杂结构和时间约束，以及潜在的故障发生。这项任务往往具有挑战性，容易出错，而且结果不容易预测。因此，系统设计人员和开发人员非常希望能够访问能够产生可靠和按构造正确的代码的丰富的自动化技术库。 在这个提案中，我们提倡使用计算和通信的形式化模型以及相关的基于模型的方法，这些方法可以从基于组件的高级模型自动构建分布式实时软件应用程序。其目标是通过使用正式定义的模型转换步骤来增加应用程序的完整性，从而产生逐个构造的更正构件。具体地说，我们将研究形式化模型，其中组件通过高级同步原语和深层次多阶段模型转换工具链相互交互，以逐个构造的正确实现结束。开发这种转换链的挑战性问题是确保它们保留高级模型的功能属性，并且可以用来使用非干扰的额外功能属性来增强生成的可执行代码。建议工作中感兴趣的属性包括容错性、时间约束和监控能力。 该项目的结果将是一个工作工具链，它为普通设计人员和工程师提供简单但高度表达的建模语言，该语言具有流行的命令式语言(如C++)的内联功能。工具链将包括一个丰富的转换算法库，用于生成分布式/多核、实时、可靠的代码。该项目的所有阶段和结果将通过使用分布式无人机应用程序进行演示。

Design and implementation of real-time distributed and multi-core systems often involves many subtleties due to their inherent complex structure and timing constraints, as well as the potential occurrence of faults. This task is often challenging, error-prone, and the outcome is not easily predictable. Thus, it is highly desirable for system designers and developers to have access to a rich library of automated techniques capable of producing dependable and correct-by-construction code. In this proposal, we advocate the use of formal models of computation and communication and associated model-based methods that automatically build distributed real-time software applications from high-level component-based models. The objective is to increase application integrity by using formally defined model transformation steps leading to correct-by-construction artifacts. Specifically, we will investigate formal models where components interact with each other through high-level synchronization primitives and deep multi-stage model transformation tool chains ending in correct-by-construction implementations. The challenging problem in developing such transformation chains is to ensure that they preserve functional properties of the high-level models and can be used to augment the generated executable code with non-interfering extra-functional properties. The properties of interest in the proposed work include fault-tolerance, timing constraints, and monitoring capabilities. The outcome of this project will be a working tool chain that provides average designers and engineers with a simple but highly expressive modeling language with inlining features for a popular imperative language such as C++. The tool chain will include a rich library of transformation algorithms for generating distributed/multi-core, real-time, dependable code. All stages and results of the project will be demonstrated by using a distributed UAV application.