search menu icon-carat-right cmu-wordmark

DMPL: Programming and Verifying Distributed Mixed-Synchrony and Mixed-Critical Software

June 2016 Technical Report
Sagar Chaki, David Kyle

DMPL is a language for programming distributed real-time, mixed-criticality software. It supports distributed systems in which each node executes a set of periodic real-time threads that are scheduled by priority and criticality.

Publisher:

Software Engineering Institute

CMU/SEI Report Number

CMU/SEI-2016-TR-005

Abstract

A language called DMPL for programming distributed real-time, mixed-criticality software is presented. DMPL supports a distributed system in which each node executes a set of periodic real-time threads that are scheduled on the basis of their priority and criticality. Both synchronous and asynchronous threads are allowed. The syntax and semantics of DMPL are formally described. A compiler that generates C++ code from a DMPL program is presented. Two methods of verification of properties of synchronous threads via sequentialization are proposed: fully-automated bounded model checking, and deductive verification with manually-supplied invariants. DMPL programming and verification are validated on several examples of collision avoidance in multi-robot systems.