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

reportActive / Technical Report | Accession Number: AD1044982 | Open PDF

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.

Author(s):
Chaki, Sagar ; Kyle, David
Author Organization(s):
CARNEGIE-MELLON UNIV PITTSBURGH PA PITTSBURGH United States
Descriptive Note:
Technical Report
Pagination:
0039

Security Markings

DOCUMENT & CONTEXTUAL SUMMARY

Distribution:
Approved For Public Release
Distribution Statement:
Approved For Public Release;

RECORD

Collection: TR
Identifying Numbers
Report Number(s):
CMU/SEI-2016-TR-005
Contract/Grant Number(s):
FA8721-05-C-0003
 Subject Terms
Joint Capability Areas:
JCA_1_Force Support; JCA_5_Command and Control; JCA_1.2_Force Preparation; JCA_4.6_Engineering; JCA_1.2.3_Educating; JCA_6_Net Centric; JCA_6.1_Information Transport; JCA_5.3_Planning; JCA_8_Building Partnerships; JCA_8.1_Communicate; JCA_8.1.3_Influence Adversary and Competitor Audiences; JCA_6.4.1_Secure Information Exchange; JCA_1.2.5_Lessons Learned; JCA_5.5.2_Task; JCA_5.5_Direct; JCA_6.4_Information Assurance; JCA_3.2_Engagement; JCA_3_Force Application; JCA_3.2.2_Non-Kinetic Means; JCA_1.2.6_Concepts
Modernization Areas:
Fully Networked C3; Cyber; Quantum Science and Computing
Communities of Interest:
Cyber
Descriptor(s):
ASYNCHRONOUS COMPUTERS, DISTRIBUTED COMPUTING, PROGRAMMING LANGUAGES, C PROGRAMMING LANGUAGE
Field(s)/Group(s):
Computer Hardware, Computer Programming and Software
Keyword(s):
DMPL(Digital Microprocessor Plotter Language), multi thread, synchronous, real time, multiagentsystems, mixed critical software, drts(distributed real time software), zsrm(Zero Slack Rate Monotonic)
Report Date:
2016 Jun 16
Creation Date:
2018 Feb 13