Software Engineering Institute | Carnegie Mellon University
Software Engineering Institute | Carnegie Mellon University

Digital Library

Technical Report

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

  • June 2016
  • By 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.
  • Cyber-Physical Systems
  • 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.

  • Download

Cite This Report

SEI

Chaki, Sagar; & Kyle, David. DMPL: Programming and Verifying Distributed Mixed-Synchrony and Mixed-Critical Software. CMU/SEI-2016-TR-005. Software Engineering Institute, Carnegie Mellon University. 2016. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=464254

IEEE

Chaki. Sagar, and Kyle. David, "DMPL: Programming and Verifying Distributed Mixed-Synchrony and Mixed-Critical Software," Software Engineering Institute, Carnegie Mellon University, Pittsburgh, Pennsylvania, Technical Report CMU/SEI-2016-TR-005, 2016. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=464254

APA

Chaki, Sagar., & Kyle, David. (2016). DMPL: Programming and Verifying Distributed Mixed-Synchrony and Mixed-Critical Software (CMU/SEI-2016-TR-005). Retrieved January 22, 2019, from the Software Engineering Institute, Carnegie Mellon University website: http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=464254

CHI

Sagar Chaki, & David Kyle. DMPL: Programming and Verifying Distributed Mixed-Synchrony and Mixed-Critical Software (CMU/SEI-2016-TR-005). Pittsburgh, PA: Software Engineering Institute, Carnegie Mellon University, 2016. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=464254

MLA

Chaki, Sagar., & Kyle, David. 2016. DMPL: Programming and Verifying Distributed Mixed-Synchrony and Mixed-Critical Software (Technical Report CMU/SEI-2016-TR-005). Pittsburgh: Software Engineering Institute, Carnegie Mellon University. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=464254

BibTex

@techreport{ChakiDMPLProgramming2016,
title={DMPL: Programming and Verifying Distributed Mixed-Synchrony and Mixed-Critical Software},
author={Sagar Chaki and David Kyle},
year={2016},
number={CMU/SEI-2016-TR-005},
institution={Software Engineering Institute, Carnegie Mellon University},
address={Pittsburgh, PA},
url={http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=464254} }