Skip to content

Clarified the inputs for the PID case study. #244

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Oct 7, 2016
Merged

Clarified the inputs for the PID case study. #244

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
3267568
Clarified the inputs for the pid case study.
theyoucheng Sep 30, 2016
cf085a8
Added the test suite for unwinding the loop 6 times in PID case study.
theyoucheng Sep 30, 2016
6266a20
Added the test suite for unwinding the loop 6 times in PID case study.
theyoucheng Sep 30, 2016
455c36b
Refined the form of test suites generated for the PID controller.
theyoucheng Oct 7, 2016
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
182 changes: 110 additions & 72 deletions doc/html-manual/cover.shtml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,13 +53,13 @@ is plotted in the Figure below.

</center>

<pre><code class="c numbered">01: // CONSTANTS:
02: #define MAX_CLIMB_SUM_ERR 100
<pre><code class="c numbered">01: // CONSTANTS:
02: #define MAX_CLIMB_SUM_ERR 10
03: #define MAX_CLIMB 1
04:
05: #define CLOCK 16
06: #define MAX_PPRZ (CLOCK*600)
07:
07:
08: #define CLIMB_LEVEL_GAZ 0.31
09: #define CLIMB_GAZ_OF_CLIMB 0.75
10: #define CLIMB_PITCH_OF_VZ_PGAIN 0.05
Expand All @@ -70,88 +70,99 @@ is plotted in the Figure below.
15: const float climb_pgain=CLIMB_PGAIN;
16: const float climb_igain=CLIMB_IGAIN;
17: const float nav_pitch=0;
18:
19: // 1) the target speed in vertical direction
20: float desired_climb;
21: // 2) vertical speed of the UAV, estimated by a control function
22: float estimator_z_dot;
23:
24: /** PID funciton OUTPUTS */
25: float desired_gaz;
26: float desired_pitch;
27: // Accumulated error in the system
28: float climb_sum_err;
29:
30: /** Computes desired_gaz and desired_pitch */
31: void climb_pid_run()
32: {
33:
34: float err=estimator_z_dot-desired_climb;
35:
36: float fgaz=climb_pgain*(err+climb_igain*climb_sum_err)+CLIMB_LEVEL_GAZ+CLIMB_GAZ_OF_CLIMB*desired_climb;
37:
38: float pprz=fgaz*MAX_PPRZ;
39: desired_gaz=((pprz>=0 && pprz<=MAX_PPRZ) ? pprz : (pprz>MAX_PPRZ ? MAX_PPRZ : 0));
40:
41: /** pitch offset for climb */
42: float pitch_of_vz=(desired_climb>0) ? desired_climb*pitch_of_vz_pgain : 0;
43: desired_pitch=nav_pitch+pitch_of_vz;
44:
45: climb_sum_err=err+climb_sum_err;
46: if (climb_sum_err>MAX_CLIMB_SUM_ERR) climb_sum_err=MAX_CLIMB_SUM_ERR;
47: if (climb_sum_err<-MAX_CLIMB_SUM_ERR) climb_sum_err=-MAX_CLIMB_SUM_ERR;
48:
49: /** Estimates the vertical speed */
50: estimator_z_dot=climb_pgain * err + desired_climb;
18:
19: /** PID function INPUTS */
20: // The user input: target speed in vertical direction
21: float desired_climb;
22: // Vertical speed of the UAV detected by GPS sensor
23: float estimator_z_dot;
24:
25: /** PID function OUTPUTS */
26: float desired_gaz;
27: float desired_pitch;
28:
29: /** The state variable: accumulated error in the control */
30: float climb_sum_err=0;
31:
32: /** Computes desired_gaz and desired_pitch */
33: void climb_pid_run()
34: {
35:
36: float err=estimator_z_dot-desired_climb;
37:
38: float fgaz=climb_pgain*(err+climb_igain*climb_sum_err)+CLIMB_LEVEL_GAZ+CLIMB_GAZ_OF_CLIMB*desired_climb;
39:
40: float pprz=fgaz*MAX_PPRZ;
41: desired_gaz=((pprz>=0 && pprz<=MAX_PPRZ) ? pprz : (pprz>MAX_PPRZ ? MAX_PPRZ : 0));
42:
43: /** pitch offset for climb */
44: float pitch_of_vz=(desired_climb>0) ? desired_climb*pitch_of_vz_pgain : 0;
45: desired_pitch=nav_pitch+pitch_of_vz;
46:
47: climb_sum_err=err+climb_sum_err;
48: if (climb_sum_err>MAX_CLIMB_SUM_ERR) climb_sum_err=MAX_CLIMB_SUM_ERR;
49: if (climb_sum_err<-MAX_CLIMB_SUM_ERR) climb_sum_err=-MAX_CLIMB_SUM_ERR;
50:
51: }
52:
53: int main()
54: {
55: /** Non-deterministic initialisation */
56: desired_climb=nondet_float();
57: estimator_z_dot=nondet_float();
58:
59: /** Range of initial values of variables */
60: __CPROVER_assume(desired_climb>=-MAX_CLIMB && desired_climb<=MAX_CLIMB);
61: __CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB);
62:
63: while(1)
64: {
65: climb_pid_run();
66: }
67:
68: return 0;
69: }
55:
56: while(1)
57: {
58: /** Non-deterministic input values */
59: desired_climb=nondet_float();
60: estimator_z_dot=nondet_float();
61:
62: /** Range of input values */
63: __CPROVER_assume(desired_climb>=-MAX_CLIMB && desired_climb<=MAX_CLIMB);
64: __CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB);
65:
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There should be two __CPROVER_input commands to record these.

66: __CPROVER_input("desired_climb", desired_climb);
67: __CPROVER_input("estimator_z_dot", estimator_z_dot);
68:
69: climb_pid_run();
70:
71: __CPROVER_output("desired_gaz", desired_gaz);
72: __CPROVER_output("desired_pitch", desired_pitch);
73:
74: }
75:
76: return 0;
77: }
</code></pre>

<p class="justified">
In order to test the PID controller, we construct a main control loop,
which repeatedly invokes the function <code>climb_pid_run</code> (line 65).
In the beginning of the main function, the values of the desired speed <code>desired_climb</code>
and the estimated speed <code>estimated_z_dot</code> are initialised non-deterministically.
Subsequently, the <code>__CPROVER_assume</code> statement in lines 60 and 61 guarantees that
their values are bounded within a range.
which repeatedly invokes the function <code>climb_pid_run</code> (line 69).
This PID function has two input variables: the desired speed <code>desired_climb</code>
and the estimated speed <code>estimated_z_dot</code>.
In the beginning of each loop iteration, values of the inputs are assigned non-deterministically.
Subsequently, the <code>__CPROVER_assume</code> statement in lines 63 and 64 guarantees that
both values are bounded within a valid range.
The <code>__CPROVER_input</code> and <code>__CPROVER_output</code> will help clarify the inputs
and outputs of interest for generating test suites.
</p>

<p class="justified">
To demonstrate the automatic test suite generation in CBMC,
we call the following command
we call the following command and we are going to explain the command line options one by one.
</p>

<pre><code>cbmc pid.c --cover mcdc --unwind 25 --trace --xml-ui
<pre><code>cbmc pid.c --cover mcdc --unwind 6 --trace --xml-ui
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am not told why "6" is the right number

</code></pre>

<p class="justified">
The option <code>--cover mcdc</code> specifies the code coverage criterion.
There are four conditional statements in the PID function: in line 39, line 42,
line 46 and line 47.
There are four conditional statements in the PID function: in line 41, line 44,
line 48 and line 49.
To satisfy MC/DC, the test suite has to meet multiple requirements.
For instance, each conditional statement needs to evaluate to <em>true</em> and <em>false</em>.
Consider the condition <code>"pprz>=0 && pprz<=MAX_PPRZ"</code> at line 39. CBMC
Consider the condition <code>"pprz>=0 && pprz<=MAX_PPRZ"</code> in line 41. CBMC
instruments three coverage goals to control the respective evaluated results of <code>"pprz>=0"</code> and
<code>"pprz<=MAX_PPRZ"</code>.
We list them in below and they satisfy the MC/DC rules.
Note that <code>MAX_PPRZ</code> is defined as 16 * 600 at line 06 of the program.
Note that <code>MAX_PPRZ</code> is defined as 16 * 600 in line 06 of the program.
</p>

<pre>
Expand All @@ -170,21 +181,48 @@ goals at the same time. Each trace corresponds to a test case.
</p>

<p class="justified">
For the example above, the following test suites are generated.
In the end, the following test suites are automatically generated for testing the PID controller.
A test suite consists of a sequence of input parameters that are
passed to the PID function <code>climb_pid_run</code> at each loop iteration.
For example, Test 1 covers the MC/DC goal with id="climb_pid_run.coverage.1".
<pre><code>Test suite:
T1: desired_climb=-1.000000f, estimator_z_dot=1.000000f
(goal id: climb_pid_run.coverage.1)
T2: desired_climb=1.000000f, estimator_z_dot=-1.000000f
(goal id: climb_pid_run.coverage.2)
T3: desired_climb=0.000000f, estimator_z_dot=0.000000f
(goal id: climb_pid_run.coverage.3)
Test 1.
(iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f

Test 2.
(iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f
(iteration 2) desired_climb=1.000000f, estimator_z_dot=-1.000000f

Test 3.
(iteration 1) desired_climb=0.000000f, estimator_z_dot=-1.000000f
(iteration 2) desired_climb=1.000000f, estimator_z_dot=-1.000000f

Test 4.
(iteration 1) desired_climb=1.000000f, estimator_z_dot=-1.000000f
(iteration 2) desired_climb=1.000000f, estimator_z_dot=-1.000000f
(iteration 3) desired_climb=1.000000f, estimator_z_dot=-1.000000f
(iteration 4) desired_climb=1.000000f, estimator_z_dot=-1.000000f
(iteration 5) desired_climb=0.000000f, estimator_z_dot=-1.000000f
(iteration 6) desired_climb=1.000000f, estimator_z_dot=-1.000000f

Test 5.
(iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f
(iteration 2) desired_climb=-1.000000f, estimator_z_dot=1.000000f
(iteration 3) desired_climb=-1.000000f, estimator_z_dot=1.000000f
(iteration 4) desired_climb=-1.000000f, estimator_z_dot=1.000000f
(iteration 5) desired_climb=-1.000000f, estimator_z_dot=1.000000f
(iteration 6) desired_climb=-1.000000f, estimator_z_dot=1.000000f
</code></pre>
</p>

<p class="justified">
The option <code>--unwind 25</code> unwinds the loop inside the main
function body 25 times. The number of the unwinding operation is
adjustable, and an introduction to the use of loop unwinding can be found
The option <code>--unwind 6</code> unwinds the loop inside the main
function body six times. In order to achieve the complete coverage on all the instrumented goals
in the PID function <code>climb_pid_run</code>, the loop must be unwound sufficient enough times.
For example, <code>climb_pid_run</code> needs to be called at least six times for evaluating the
condition <code>climb_sum_err>MAX_CLIMB_SUM_ERR</code> in line 48 to <em>true</em>.
This corresponds to the Test 5.
An introduction to the use of loop unwinding can be found
in <a href="cbmc-loops.shtml">Understanding Loop Unwinding</a>.
</p>

Expand Down
39 changes: 22 additions & 17 deletions doc/html-manual/pid.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
// CONSTANTS:
#define MAX_CLIMB_SUM_ERR 100
#define MAX_CLIMB_SUM_ERR 10
#define MAX_CLIMB 1

#define CLOCK 16
Expand All @@ -16,17 +16,18 @@ const float climb_pgain=CLIMB_PGAIN;
const float climb_igain=CLIMB_IGAIN;
const float nav_pitch=0;

// 1) the target speed in vertical direction
/** PID function INPUTS */
// The user input: target speed in vertical direction
float desired_climb;
// 2) vertical speed of the UAV detected by GPS sensor
// Vertical speed of the UAV detected by GPS sensor
float estimator_z_dot;

/** PID funciton OUTPUTS */
/** PID function OUTPUTS */
float desired_gaz;
float desired_pitch;
// Accumulated error in the system
float climb_sum_err;

/** The state variable: accumulated error in the control */
float climb_sum_err=0;

/** Computes desired_gaz and desired_pitch */
void climb_pid_run()
Expand All @@ -47,25 +48,29 @@ void climb_pid_run()
if (climb_sum_err>MAX_CLIMB_SUM_ERR) climb_sum_err=MAX_CLIMB_SUM_ERR;
if (climb_sum_err<-MAX_CLIMB_SUM_ERR) climb_sum_err=-MAX_CLIMB_SUM_ERR;

/** The control function for estimating the vertical speed */
estimator_z_dot=climb_pgain * err + desired_climb;

}


int main()
{
/** Non-deterministic initialisation */
desired_climb=nondet_float();
estimator_z_dot=nondet_float();

/** Range of initial values of variables */
__CPROVER_assume(desired_climb>=-MAX_CLIMB && desired_climb<=MAX_CLIMB);
__CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB);

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

climd_sum_err should be initialized explicitly

while(1)
{
/** Non-deterministic input values */
desired_climb=nondet_float();
estimator_z_dot=nondet_float();

/** Range of input values */
__CPROVER_assume(desired_climb>=-MAX_CLIMB && desired_climb<=MAX_CLIMB);
__CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB);

__CPROVER_input("desired_climb", desired_climb);
__CPROVER_input("estimator_z_dot", estimator_z_dot);

climb_pid_run();

__CPROVER_output("desired_gaz", desired_gaz);
__CPROVER_output("desired_pitch", desired_pitch);

}

return 0;
Expand Down