Verifying Distributed Adaptive Real-Time (DART) Systems

Abstract

Distributed Adaptive Real-Time (DART) systems are key to many areas of DoD capability (e.g., autonomous multi-UAS missions) with civilian benefits. However achieving high assurance DART software is very difficult Concurrency is inherently difficult to reason about. Uncertainty in the physical environment. Autonomous capability leads to unpredictable behavior. Assure both guaranteed and probabilistic properties. Verification results on models must be carried over to source code. High assurance unachievable via testing or ad-hoc formal verification

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 08, 2015
Accession Number
AD1128225

Entities

People

  • Dionisio de Niz
  • Sagar Chaki

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Air Platforms

DTIC Thesaurus Topics

  • Area Coverage
  • Autonomous Systems
  • Collision Avoidance
  • Collisions
  • Computer Programming
  • Computer Programs
  • Contracts
  • Control Systems
  • Department Of Defense
  • Engineering
  • Guarantees
  • Language
  • Materials
  • Models
  • Probabilistic Models
  • Programming Languages
  • Software Development
  • Universities
  • Verification
  • Virtual Machines

Fields of Study

  • Computer science

Readers

  • Adaptive Control and Estimation with Uncertainty in Dynamic Systems.
  • Software Engineering.
  • Unmanned Aerial System (UAS) Autonomous Capabilities and Mission Reconnaissance.