search menu icon-carat-right cmu-wordmark

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

Technical Report
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
DOI (Digital Object Identifier)
10.1184/R1/6573233.v1

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.

Cite This Technical Report

Chaki, S., & Kyle, D. (2016, June 21). DMPL: Programming and Verifying Distributed Mixed-Synchrony and Mixed-Critical Software. (Technical Report CMU/SEI-2016-TR-005). Retrieved February 23, 2024, from https://doi.org/10.1184/R1/6573233.v1.

@techreport{chaki_2016,
author={Chaki, Sagar and Kyle, David},
title={DMPL: Programming and Verifying Distributed Mixed-Synchrony and Mixed-Critical Software},
month={Jun},
year={2016},
number={CMU/SEI-2016-TR-005},
howpublished={Carnegie Mellon University, Software Engineering Institute's Digital Library},
url={https://doi.org/10.1184/R1/6573233.v1},
note={Accessed: 2024-Feb-23}
}

Chaki, Sagar, and David Kyle. "DMPL: Programming and Verifying Distributed Mixed-Synchrony and Mixed-Critical Software." (CMU/SEI-2016-TR-005). Carnegie Mellon University, Software Engineering Institute's Digital Library. Software Engineering Institute, June 21, 2016. https://doi.org/10.1184/R1/6573233.v1.

S. Chaki, and D. Kyle, "DMPL: Programming and Verifying Distributed Mixed-Synchrony and Mixed-Critical Software," Carnegie Mellon University, Software Engineering Institute's Digital Library. Software Engineering Institute, Technical Report CMU/SEI-2016-TR-005, 21-Jun-2016 [Online]. Available: https://doi.org/10.1184/R1/6573233.v1. [Accessed: 23-Feb-2024].

Chaki, Sagar, and David Kyle. "DMPL: Programming and Verifying Distributed Mixed-Synchrony and Mixed-Critical Software." (Technical Report CMU/SEI-2016-TR-005). Carnegie Mellon University, Software Engineering Institute's Digital Library, Software Engineering Institute, 21 Jun. 2016. https://doi.org/10.1184/R1/6573233.v1. Accessed 23 Feb. 2024.

Chaki, Sagar; & Kyle, David. DMPL: Programming and Verifying Distributed Mixed-Synchrony and Mixed-Critical Software. CMU/SEI-2016-TR-005. Software Engineering Institute. 2016. https://doi.org/10.1184/R1/6573233.v1