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

点击翻译按钮获取中文摘要

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.