DRREACH

Grant

This project is supported by the Air Force Office of Scientific Research (AFOSR) through contract number FA9550- 8-1-0122 and the Defense Advanced Research Projects Agency (DARPA) through contract number FA8750-18-C-0089 (the DARPA Assured Autonomy Project) .

Motivation

Safety-critical distributed cyber-physical systems (CPSs) have been found in a wide range of applications. Notably, they have displayed a great deal of utility in intelligent transportation, where autonomous vehicles communicate and cooperate with each other via a high-speed communication network. Such systems require an ability to identify maneuvers in real-time that cause dangerous circumstances and ensure the implementation always meets safety-critical requirements. In the case that a dangerous circumstance may happen, the system should have ability to perform safe motion planning to escape from that dangerous situation. Last but not least, an intelligent distributed CPS should have ability to verify the safety and perform safe motion planning when there are human in the loop .

Objectives & Publications

• Decentralized Real-time Verification for Distributed Autonomous Cyber-Physical Systems

  • FORTE'19, ARCH'17

• Verification-guided Motion Planning for Distributed Autonomous Cyber-Physical Systems

  • On-going

• Decentralized Real-time Verification for Distributed Cyber-Physical Systems with Human in the Loop

• Verification-guided Motion Planning for Distributed Cyber-Physical Systems with Human in the Loop

Approach

For objective 1, we propose a real-time decentralized safety verification approach for a distributed multi-agent CPS with the underlying assumption that all agents are time-synchronized with a low degree of error. In the proposed approach, each agent periodically computes its local reachable set and exchanges this reachable set with the other agents with the goal of verifying the system safety. Our method, implemented in Java, takes advantages of the timing information and the reachable set information that are available in the exchanged messages to reason about the safety of the whole system in a decentralized manner. Any particular agent can also perform local safety verification tasks based on their local clocks by analyzing its local reachable set and safety specifications.

Tool

• drreach a java package developed on top of StarL, a novel platform-independent framework for programming reliable distributed robotics applications on Android.

Applications

Verification of Distributed Search using Quadcopter