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

Digital Library

Javascript is currently disabled for your browser. For an optimal search experience, please enable javascript.

Advanced Search

Basic Search

Content Type

Topics

Publication Date

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 September 24, 2018, 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} }