Benchmarks

About the tool-chain

Our tool-chain takes 1) plant model as hybrid automaton, 2) Controller program in C with standard input/output structures, 3) Configuration file with real-time disturbance(Jitter, Noise, Quantization error) specifications. It merges this implementation level details and encodes an SMT formula over Reals, to be solved by dReal Solver.

Execution Details

To run the tool with the plant model as "benchmarks/thermostat.ha" and controller program as "benchmarks/thermostat.c" having the header file "thermostat.h" in the same "benchmarks", with the sampling time of the controller as "0.2", for the time-horizon of "3" units, type the command as given below. Details about in line parameters are given below or else all these information can be input in configuration file.

$ ./SaVerECS -m 100 -t 0.2 -d 0.001 -u 10 -l 5 --time-horizon 3 --goal "x>=5 & y>=3" --plant-file "benchmarks/thermostat.ha" --controller-file "benchmarks/thermostat.c" -o test.smt2

For example to get help on using the tool's CLI commands type the following:

$ ./SaVerECS --help

-h [ --help ] Produce help message

-m [ --max-value ] arg Assumed maximum [-m, +m] constant value that the plant and the controller can take

-t [ --sampling-time ] arg Sets the sampling time of the controller

-r [ --release-time ] arg Sets the release time of the controller

-d [ --sensing-time ] arg Sets the sensing time of the controller

--precision arg set precision for the SMT solver (default 0.001)

-u [ --upper-bound ] arg Set the depth or upper-bound of exploration for unrolling

-l [ --lower-bound ] arg Set the depth or lower-bound of exploration for unrolling

-Z [ --time-horizon ] arg Set the global time horizon of computation.

-F [ --goal ] arg Goal property to test, syntax: 'expr-1 &

expr-2'; For e.g. expr-1 is x>=2 expr-2 is x<=(-2)

--noise-params arg Sets the noise injecting parameters, syntax:

'var1:[t1,t2]=>[n1,n2] & ...'where t1 and t2 are start and end time duration of

the noise on var1 and the noise values can be fix [n1,n1] or range [n1,n2]

--disturbance arg Sets the disturbance parameters, syntax:

'var1:[t1,t2]=>[d1,d2] & ...'where t1 and t2 are start and end time duration of

the disturbance on var1 and the disturbance values can be fix [d1,d1] or range [d1,d2]

-I [ --include-path ] arg include file path

-p [ --plant-file ] arg include plant model file

-c [ --controller-file ] arg include controller C program file

-g [ --config-file ] arg include configuration file (for future use)

-o [ --output-file ] arg output file name for redirecting the outputs (example .smt2 file)

Input files

Controller Code

The input and the output argument variables are declare in a structure within a header file (controller.h) which is included in the controller program (controller.c). The names of the structure should be INPUT_VAL and RETURN_VAL as shown below:

typedef struct{ datatype outputVarName;
}RETURN_VAL;
typedef struct{ datatype plantVarName; //The value sensed from the plant (remember to follow the same naming convension in the plant model as well. In addition, we use the key word "state_" as a prefix before the sensed variables of the plant and prefix by the key word "next_" to the output variables that is returned from the controller program.)
datatype otherControllerVarName;
}INPUT_VAL;

The header file (for eg controller.h) should also include the declaration of the controller function as shown below:

datatype controller(INPUT_VAL* iv, RETURN_VAL* rv); //here the return datatype can be void, e.t.c. Note that we assume all controller program begin with the function name as "controller()" just like a C/C++ program begin with the function main().

We also assume that the definition of the function follows the following usual pattern as reflected below. Note that we pass the arguments as reference variables, so we do not use the return statement to return the parameter.

#include "controller.h" //contains the structure declaration as shown in 1) and 2) above.
void controller(INPUT_VAL* input, RETURN_VAL* ret_val) {
//local varaible declaration // ============================ datatype v1,v2, ...., vn;
// retrieving values from the input varaibles onto the local variables // ==================================================================== v1 = input->plantVarName; v2 = input->otherControllerVarName
// performing the logic of the controller program //==================================================================== //actual calculation and taking logical decisions, etc
....
//Finally, update the computed values to the output variable and changing the current state of the controller(input variables) in the data structures //============================================================================================================================================== ret_val->outputVarName = vn; input->otherControllerVarName = vj; //e.t.c.,
}

Configuration File

#Possible values here are: 1) MinMax-bounds of variables (plant and controller) 2)comments line begin with # or // 3) max-value 4) --sampling-time 5) release-time 6) sensing-time or sampling jitter 7) upper-bound 8) lower-bound 9) time-horizon 10) goal 11) noise-params 12 ) disturbance

Plant Description

module modelname(state,control variables...) output output variables...;
%location details mode loc begin ddt x1 = (-50/1000)*v + (1/1000)*u;% flow equation . . % other flow equations end% initial states initial begin set begin mode == loc; x1 <= 80; x1 >= 50; . . % other state,control input initializations end endendmodule

for more details refer ForFET: A Formal Feature Evaluation Tool for Hybrid Systems

output files

Every benchmark folder contains

## .ha file : containing Initial states and plant model

## .c, .h file : with controller code, along with standard input output format in header file

## .cfg file: with several implementation level details(Variable ranges, disturbances), Safety property and bound to be checked for

## output folders

with sample runs as reported in paper,

### .log files: with execution time logs,
### .smt2 files: containing tool generated smt formula in smt-lib 2.0 format,
### .json files: to visualize counter examples (instructions given in .log file)

Benchmark Details

Thermostat

Initial Plant State: 55 F =<temperature<= 75
Initial Control Input : u =20
Tested Mode : All three (Off, RegularHeating and FastHeating)
Safety Criteria : temperature < 52
Tested Disturbances : release-time = 0.1, sampling jitter = 0.1

DC Motor

Initial Plant State: 1=< armature current <=1.2, 10 =<angular velocity (theta dot)<=11
Initial Control Input : voltage = 1
Safety Criteria : 1.0 =< i<=1.2 & 11 =< angVal>=10
Tested Disturbances : release-time = 0.01, sensing-time = 0.001

Yaw Damper for Boeing 747

Initial Plant State: 0.226891=< x1 <= 0.318401 ;1.384075 =<x2 <= 1.625669 ; 0.226891 =<x3 <= 0.318401 ; 1.384075 =<x4 <= 1.625669 ; 1.384075=< w <= 1.625669 ;
Initial Control Input : 0.226891=<u <= 0.318401 ;
Tested Mode : Spiral Mode
Safety Criteria : x4<=0.08

Powertrain

Initial Plant State: 115.19 =< p_engine_speed >= 94.25; p_throttle_angle == 9.9; p_manifold_pressure==0.7840; p_airbyfuel_meas==14.7; in_thetaI == 10;
Initial Control Input : c_commanded_fuel_gps == 0.3517 ; p_air_estimate == 0.784; p_pi == 0;
Tested Mode : Normal Mode
Safety Criteria : p_airbyfuel_meas>15
Tested Disturbances : release-time = 0.01

Lunar Lander

Initial Plant State: 29.5 =<position <=30.5; -2.5=< velocity <= -1.5; 1245 =<mass <= 1255;
Initial Control Input : 2020 =<FuelCommand <= 2035; tempM == 0 ; tempF == 0 ;
Safety Criteria : position==0 & 5<velocity<(-5)
Tested Disturbances : time: [0.1,0.5] =>angVal:[-0.02,+0.02]

Adaptive Cruise Control

Initial Plant State: 50 =< velocity <= 80; 40 =< acceleration <= 70;
Initial Control Input : 450 =< u <= 500;
Tested Mode : Car Following Mode
Safety Criteria : time >=0.4 & velocity >11
Tested Disturbances : release-time = 0.02, sampling jitter = 0.012

Electro-Magnetic Break

Initial Plant State: Motor Current==0; Caliper Position==0;
Initial Control Input : Voltage==0; Xc==0;
Safety Criteria : Caliper Position>0.052 & time <0.146
Tested Disturbances : sensing-time = 0.001

Benchmark Repository

Page updated

Google Sites

Report abuse