Engineering High-Assurance Software for Distributed Adaptive Real-Time Systems (Keynote)

Sagar Chaki, Midwest Verification Day (MVD), October 21-22, 2016, Ames, IA, USA.

Abstract: Distributed Adaptive Real-Time (DART) systems are cyber-physical systems with physically separated nodes that communicate and coordinate to achieve their goals, and self-adapt to their environment to improve likelihood of success. DART systems promise to revolutionize several domains that impact our daily lives in critical ways, such as robotics, transportation, energy, and healthcare. 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 domain specific languages with precise semantics, rigorous analysis, and design constraints, which leads to assured behavior of DART systems.