Modeling, Verifying, and Generating Software for Distributed Cyber-Physical Systems using DMPL and AADL.
• Conference Paper
Software Engineering Institute
The Distributed Adaptive Real-Time (DART) project at the Carnegie Mellon Software Engineering Institute has been developing an engineering method for producing high-assurance software for cyber-physical systems composed of multiple agents (such as a team of robots) that communicate, coordinate, and adapt to uncertain environments in order to achieve safety-critical and mission-critical goals. We have developed an executable domain specific language, called DMPL, to program DART systems, verify safety and probabilistic properties, prove real-time schedulability, and ultimately generate C++ code to be compiled and deployed on a target platform. Using DMPL, we have developed a number of multi-agent scenarios that incorporate verified collision-avoidance protocols, mixed-criticality real-time scheduling, and proactive self-adaptation algorithms. More details are available at https://github.com/cps-sei/dart. More recently, we have integrated DMPL with the AADL/OSATE ecosystem by developing an AADL annex. This provides an end-to-end framework where DART systems can be designed, analyzed, and implemented within the same toolchain. In this talk, we will present this toolchain and demonstrate it on a few representative examples.