search

saverecs / SaverECS

SaverECS : A safety verification tool for verification of embedded control software running in closed-loop with plants, under perturbations and different scheduling scenarios.
1 stars 3 forks source link
embedded-software smt verification

readme 

Indian Institute of Technology Kharagpur, India,
Formal Methods Lab,
Project Title: "FMSAFE: A Networked Centre for Formal Methods in Validation and Certification Procedures for Safety Critical ICT Systems"

Funded by IMPRINT, a MHRD supported Pan-IIT + IISc joint initiative for addressing major science and engineering challenges that are relevant in the national context.

Copyright (c) 2018 Formal Methods Lab, Indian Institute of Technology Kharagpur, India.

Tool Developer:
           Amit Gurung,
           Jay Thakkar,                
           Sunandan Adhikary,
           Antonio Bruto da Costa

Safety Verification of Embedded Control Software Tool-chain

SaVerECS is an SMT-based verification tool to formally guarantee the performance and safety of an embedded control software under the influence of process or measurement noises and timing uncertainties (delay, jitters), before implementing them in real-time systems. Support for non-linearities in the controlled plant and the controller software, real-valued constraints and control software code as input, make this tool-chain ideal for verifying real-world hybrid systems. Our tool incorporates semantic support for capturing plant specifications, timing and value-based uncertainties (noise, precision errors), and the control software code.

Evaluated verification benchmarks can be found in this repository. The operational details of the designed tool-chain are documented here.

Prerequisite (for running the tool):

1) clang and llvm 
$ sudo apt-get install clang
$ sudo apt-get install llvm
2) boost library for c++
$ sudo apt-get install libboost-all-dev

How to build: 

To generate the executable, type the following command in the terminal:

    $ cd fmsafe/src
    $ ./compile-cpp

Note:

Input Format:

1) 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 convention in the plant model). In addition, we use the keyword "state_" as a prefix before the sensed variables of the plant and prefix by the keyword "next_" to the output variables that are returned from the controller program.

                datatype otherControllerVarName;   

            }INPUT_VAL;

2) 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, etc.
        Note that we assume all controller programs begin with the function name as "controller()," just like a C/C++ program begins with the function main().

3) 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 variable declaration 
                ============================
                    datatype v1,v2, ...., vn;

                retrieving values from the input variables 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 change the controller's current state (input variables) in the data structures.
                ==============================================================================================================================================
                ret_val->outputVarName = vn;
                input->otherControllerVarName = vj; //etc.,

            }

Detailed Command Line Interface (CLI):

    -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)

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

    $ ./SaVerECS  --help

2) To run the tool with the plant model as "benchmarks/thermostat/thermostat.ha" and controller program as "benchmarks/thermostat/thermostat.c" having the header file "thermostat.h" in the same "benchmarks/thermostat/," with the sampling time of the controller as "0.2", for the time-horizon of "3" units, type the command as given below. The output is generated in the file "test.smt2" using the -o flag. The number of depth for unrolling is specified by -u and -l, where u is the upper-bound and l the lower-bound. The flag -m is to supply a maximum bound for all variables (both plant and controller) within which the variables always lie. The flag -d is used to input the sensing time. For simple goal/property to test, use the --goal flag.

    $ ./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

3) Else one can simply input all these values in configuration file as ` benchmarks/thermostat/thermostat.cfg ` and run the following to verify the goal property,

    $ ./SaVerECS -g "benchmarks/thermostat/thermostat.cfg" --plant-file "benchmarks/thermostat/thermostat.ha" --controller-file "benchmarks/thermostat/thermostat.c" -o benchmarks/thermostat/outputs/thermostat

How to Run:

To execute the project with sample test inputs,

Note:

To visualize the output counterexample trace, follow the on-screen instructions i.e., Copy the .json file content to ../ODE_Visualization/data.json and run the following in terminal and view in localhost:8000 URL.

$ ./run_websvr.sh

Don't forget to run the following, in the end, to shut down the localhost.

$ ./shut_websvr.sh

Benchmarks

Benchmarks Run using our Tool-chain is in this repository. You can also visit this link for details.

An Example of SMT Encoding

Mathematical formulae to represent a closed-loop system into SMT encoding is shown below. The process of generating the SMT formula for a DC Motor system (refer to this work) is presented as an example. This DC Motor system has two states (x), i.e. angular velocity (angVal) and armature current (i), being controlled by a PI controller using a control variable (u) i.e. voltage. The PI controller's goal is to reduce error in plant's output, caused by bounded additive noise (w) introduced during run-time.

Note: The presented SMT-LIB2 format of the formula contains plant and Controller flow during the first sampling instance. gt and lt are two variables denoting global time and local time of the system. The first suffix i.e., 0 introduced in each variable, corresponds to the first iteration/sampling period. The second suffix i.e., 0 or t corresponds to flow of the variables, e.g., angVal_0_0 and angVal_0_t are values of angular velocity at the start of the zeroth iteration and the end of the zeroth iteration respectively.]

  1. The Plant model (using the HASLAC format) is:

    module dcmotor(angVal, i, voltage)

    output angVal, i;

    mode loc
        begin
            ddt angVal =  (-0.1/0.01)*angVal + (0.01/0.01)*i;
            ddt i = ((0.01/0.5)*angVal - (1/0.5)*i) + (voltage/0.5);
        end
    initial begin
        set begin
            mode == loc;
            angVal>=0;
            angVal<=0.2;
            i==0;
            voltage==1.0;
        end
    end
endmodule

Note that the SMT-LIB2 format is a prefix notation.

  1. The PI Controller as a C-Program.
#include "dcmotor.h"

#define SAT (20.0)
#define UPPER_SAT (SAT)
#define LOWER_SAT (-SAT)

void* controller(INPUT_VAL* input, RETURN_VAL* ret_val)
{
  double pid_op = 0.0;
  double KP = 40.0;
  double KI = 1.0;

  double error, error_i;

  double y = input->state_angVal;
  // get the previous error
  double error_i_prev = input->state_error_i_previous;
  double ref = 1.0;

  // error computation is affected by bounded sensor noise
 // error = ref - (y + input->state_angVal);
 error = ref - y;

  // to illustrate: ei += e*Ki
  error_i = error * KI + error_i_prev;
  error_i_prev = error_i;

  pid_op = error * KP + error_i * KI;

  if(pid_op > UPPER_SAT)
    pid_op = UPPER_SAT;
  else if(pid_op < LOWER_SAT)
    pid_op = LOWER_SAT;
  else
    pid_op = pid_op;

  ret_val->next_voltage = pid_op;
  input->state_error_i_previous = error_i_prev;

  return (void*)0;
}
// ***** The Header Program:  dcmotor.h *****
typedef struct{
    double next_voltage;
}RETURN_VAL;

typedef struct{
    double state_angVal;
    double state_error_i_previous;
}INPUT_VAL;

void* controller(INPUT_VAL* iv, RETURN_VAL* rv);

// ***** End of The Header Program: dcmotor.h *****

  1. The Configuration file :

    max-value = "1000"
minmax-bounds = "i:[0,2] & angval:[1,30]"
sampling-time = 0.02
release-time = 0
sensing-time = 0
Noise-params = "angVal:[0.02,1]=>[0.1,0.5]"
time-horizon = 3
upper-bound = 50
lower-bound = 1
goal ="i<=1.2 & i>=1.0 & angVal>=10 & angVal<=11"

  1. For a verification boundN=50the final SMT formula becomes:

    overall

  1. This SMT constraint is input to the dReal SMT solver, which eventually solves the ODEs. dReal SMT solver uses CAPD DynSys library to solve the ODEs over Reals.