Sagar Chaki

DRONE-PP is a development and verification platform for software executing on flying robots. Our current target is the Parrot ARDrone. The software is a periodic program written in C. It consists of a set of tasks, each executing periodically in a separate thread. Threads are scheduled pre-emptively based on their priorities. Safety properties are encoded as assertions in the C code. For a more formal description of periodic programs, see this paper. DRONE-PP works in two modes:

• Verification: It verifies the safety property using Rek as the backend engine.
• Compilation: It generates a binary that can be executed on the robot.

An important principle behind DRONE-PP is that the same C code is handled in both modes, i.e., WYVIWYR (What You Verify Is What You Run). Here is a simple example demonstrating the usage of DRONE-PP. DRONE-PP is part of the START project at the SEI.

Software: We are planning to release the DRONE-PP software. Check back periodically.

• Time-Bounded Analysis of Real-Time Systems (FMCAD'11)
• Compositional Sequentialization of Periodic Programs (VMCAI'13)
• Verifying Periodic Programs with Priority Inheritance Locks (FMCAD'13)