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.