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

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 16, 2016
Accession Number
AD1044982

Entities

People

  • David Kyle
  • Sagar Chaki

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • C4I
  • Cyber
  • Engineered Resilient Systems

DTIC Thesaurus Topics

  • Autonomous Systems
  • C Programming Language
  • Collision Avoidance
  • Collisions
  • Computer Programming
  • Computer Science
  • Computers
  • Engineering
  • Language
  • Linguistics
  • Materials
  • Operating Systems
  • Programming Languages
  • Robots
  • Software Development
  • Verification
  • Websites

Fields of Study

  • Computer science
  • Engineering

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Artificial Intelligence
  • Nanofabrication and Microfabrication.

Technology Areas

  • AI & ML
  • AI & ML - Autonomous Systems
  • AI & ML - Machine Learning Algorithms
  • Autonomy
  • Autonomy - Autonomous System Control
  • Autonomy - Human-Robot Interaction