Sagar Chaki

We illustrate DRONE-PP on an example with two tasks. Here is the overall code. The main components of the code are as follows. First, we include the DRONE-PP header file.

#include "dropnepp.h"
		

Next, we define the tasks. Each task has three functions – one that is executed only at startup, another that is executed periodically, and a third function that is executed when the task is destroyed (just before the application terminates). For example, here is the function for task2 that is executed periodically.

CODE LISTING
		

Using the Rek convention, shared variables are written and read using the functions R() and W(). Note that the shared variable ard_curr_cmd is the way the software sends commands to the ARDrone. Simply setting the value of this variable will result in the corresponding command being sent to the drone. Technically, this is done by a high priority task that has a period od 30ms and is invisible to the application. The reason we do this is because according to ARDrone documentation, sending a command every 30ms keeps the drone stable. Here is the periodic code for task1.

CODE LISTING
		

Note that the ASSERT_EMERGENCY macro sends an EMERGENCY_LAND command to the drone causing it to crash. We expect that for a correct controller, this should never happen. In this example however, if the macro BUG is defined, then there are race conditions that cause the assertion to fail. If BUG is undefined, then the LOCK() and UNLOCK() commands eliminate all the race conditions. The LOCK() function disables scheduling (between the application tasks only, not other tasks such as the high priority 30ms task) by raising the priority of the calling thread to an appropriately high value. The UNLOCK() function re-enabled the scheduler. Finally, we declare the total running time of the program (in this example, 15s), and register the two tasks.

CODE LISTING
		

Note that we declare task1 to have a period of 50ms, a WCET of 1ms, an initial arrival time of 200ms, and a priority of 6. Similarly, task2 has a period of 500ms, a WCET of 180ms, an initial arrival of 100ms, and priority of 5. Currently, DRONE-PP requires that tasks have a priority between 1 and 48. These restrictions will be relaxed in future versions of DRONE-PP. The WCET value is used for verification only and assumed to be a safe over-approximation. At runtime, if a job misses its deadline (implicitly assumed to be equal to its period) then future jobs are skipped till the next job whose arrival time is no less than the current time. This is enforced by the DRONE-PP runtime.

Running DRONE-PP: DRONE-PP has a very simple usage:

CODE LISTING
		

Using DRONE-PP to Verify: If we verify our example program with the bug enabled, DRONE-PP reports a counterexample:

CODE LISTING
		

Without the bug, DRONE-PP verifies the program to be correct.

CODE LISTING
		

Using DRONE-PP to Compile: DRONE-PP also generates executables that are linked against its runtime. If we compile with the bug enabled, and execute the resulting binary on an ARDrone, then we should see it crash. Here is the command line:

CODE LISTING
		

And here is a video of the crash. The output from the software is illustrative:

CODE LISTING
		

We see that the drone receives the TAKEOFF and HOVER commands, but then something goes wrong and it receives the EMERGENCY command instead of LAND. If we compile without the bug, the drone should takeoff, hover for about 5 seconds, and then land gracefully. Here is the command line:

CODE LISTING
		

And here is a video of the safe landing. The output of the software is as follows:

CODE LISTING
		

This time, everything goes well. The drone receives the TAKEOFF, HOVER and LAND commands in the right order as expected. Note that the CPU lock is acquired and released each time a new command is issued, as expected.