Accession Number:

AD1044982

Title:

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

Descriptive Note:

Technical Report

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA PITTSBURGH United States

Personal Author(s):

• Chaki,Sagar
• Kyle,David

Report Date:

2016-06-16

Pagination or Media Count:

39.0

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.

Descriptors:

• ASYNCHRONOUS COMPUTERS
• DISTRIBUTED COMPUTING
• PROGRAMMING LANGUAGES
• C PROGRAMMING LANGUAGE

Subject Categories:

• Computer Hardware
• Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE