Formal Synthesis and Verification Techniques for Autonomous Cyber-Physical Systems

ABSTRACT: SIFT's Phase 2 Hy-CIRCA proposal builds on progress in Phase 1 to address the challenge of effectively, reliably, and safely tasking cooperating teams of autonomous cyber-physical systems (CPSs). SIFT's Playbook(tm) interface approach provides high-level, goal-based tasking for multi-agent autonomous missions. SIFT's Cooperative Intelligent Real-Time Control Architecture (CIRCA) automatically synthesizes correct-by-construction real-time, closed loop discrete controllers for multi-agent autonomous missions. To fully realize the potential of CIRCA and Playbook, we must extend them to handle CPSs with complex, nonlinear dynamics. Recently, Professor Ed Clarke's group at Carnegie-Mellon University (CMU) has developed a novel approach to verification of nonlinear hybrid systems. CMU's dReach/dReal system uses "delta-Complete" approximate reasoning methods to model check and verify hybrid system models including nonlinear constraints, ordinary differential equations (ODEs), and discrete dynamics. SIFT and CMU will team to build Hy-CIRCA, a system that will automatically synthesize and verify closed-loop hybrid controllers based on high-level mission specifications. Hy-CIRCA will incorporate advances in reasoning about hybrid non-linear systems, hierarchical task network planning, SMT solving, and controller synthesis.; BENEFIT: The Hy-CIRCA project has potential benefits in three areas: (1) assured mission control of teams of multiple autonomous systems, the direct topic of the proposal, through construction of the integrated Hy-CIRCA system; (2) improvements in the state of the art in hybrid (cyber-physical system) verification for non-linear systems through development of improved versions of CMU's dReach/dReal tool; (3) improved planning facilities through development of improved versions of the SHOP2 HTN planner. Commercialization opportunities include licensing the Hy-CIRCA software to space and defense contractors. Another route would be to integrare the Hy-CIRCA software into software design tool suites such as Matlab/Simulink, SCADE, ESTEREL, or Modelica.