Distributed Adaptive Real-Time (DART) systems are cyber-physical systems (CPS) with physically separated nodes that communicate and coordinate to achieve their goals and that self-adapt to their environment to improve likelihood of success. DART systems promise to revolutionize several areas of civilian and Department of Defense interest, such as robotics, transportation, energy, and health care. However, to fully realize this potential, the software controlling DART systems must be engineered to have high-assurance and certified to operate safely and effectively.
Achieving this goal is challenging—and infeasible with current testing-based approaches—due to complexity resulting from concurrency and coordination, environment uncertainty, and unpredictable system evolution caused by (self-)adaptation. In this talk, we present a sound engineering approach based on judicious use of domain-specific languages with precise semantics, rigorous analysis, and design constraints that leads to assured behavior of DART systems. Our approach uses a synergistic combination of analyses from different scientific domains. It is designed to assure, in a scalable manner, critical timing and functional and probabilistic requirements for systems with uncertain environments and coordination. We have implemented our approach in a workbench, and evaluated it on a model problem. As part of this research, we have combined architecture-based analysis with state-of-the-art verification algorithms for real-time schedulability of mixed-criticality systems, software model checking, and statistical model checking, along with proactive self-adaptation and middleware technology. The result is an evidence-based approach for producing high-assurance DART software involving multiple layers of the CPS stack. We conclude with open problems and directions for future work.
