Creating a New Language to Verify Complex Systems
Distributed, adaptive real-time (DART) systems (e.g., UAS) are key to DoD capability. These systems are safety critical, resource constrained, and sensor rich, and they adapt autonomously to their physical environments.
In general, formally verifying a DART system is intractable. Coordination, adaptation, and uncertainty pose key challenges to assuring their safety- and mission-critical behavior. The typical approach to verifying DART systems is to test rigorously and exhaustively. Testing, however, is usually performed later in development and cannot account for all reactions of an essentially autonomous system.
One innovative approach that SEI researchers are using involves creating a new programming language for DART systems called the DART Modeling and Programming Language (DMPL). DMPL is a C-like language that can express distributed, real-time systems. The semantics of this language are precise; it supports formal assertions usable for model checking and probabilistic model checking. In addition, in DMPL physical and logical concurrency can be expressed in sufficient detail to perform timing analysis.
The SEI's investigation into verifying DART systems will also produce other tools for mixed criticality scheduling and model checking. In addition, work to verify DART systems continues longer term SEI research into mixed-criticality and real-time scheduling, model checking, and high-confidence cyber-physical systems (HCCPS).