Modeling, Verifying, and Generating Software for Distributed Cyber-Physical Systems using DMPL and AADL (Abstract Only)

Sagar Chaki, Dionisio de Niz, Joseph Seibel, ACM SIGAda’s High Integrity Language Technology International Workshop on Model-Based Development and Contract-Based Programming (HILT), October 6-7, 2016, Pittsburgh, PA, USA.

Abstract: 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.