search menu icon-carat-right cmu-wordmark

Verifying Distributed Adaptive Real-Time (DART) Systems

This 2015 Research Review presentation describes the authors' research efforts in verifying distributed adaptive real-time systems.

Software Engineering Institute



This research is producing the DART Modeling and Programming Language (DMPL), a C-like language that can express distributed, real-time systems. DMPL semantics are precise, and it supports formal assertions usable for model checking and probabilistic model checking. In DMPL, physical and logical concurrency can be expressed in sufficient detail to perform timing analysis.