Model Checking Laboratory

QKS

Details

Category: Software

Last Updated on Friday, 22 March 2019 14:15

QKS [TOSEM14] is a tool for automatic synthesis of correct-by-construction control software (as C code) for Discrete Time Linear Hybrid Systems. More in detail, QKS outputs a control software for software-based control systems like the following:

where we highlight the fact that:

1. measures from plant sensors go through an Analog-to-Digital (AD) conversion (quantization) before being processed;
2. the control software is typically executed by a microcontroller.

Accordingly, QKS input is the following:

1) a model of the controlled system (plant) as a Discrete Time Linear Hybrid System (DTLHS), that is a discrete time hybrid system whose dynamics is defined as a linear predicate (i.e., a boolean combination of linear constraints) on its variables;

2) system level safety specifications;

3) system level liveness specifications (as always in control problems, liveness constraints define the goal states, i.e. the set of states that any evolution of the closed loop system should eventually reach);

4) system level desired controllable region specifications;

5) a quantization schema, i.e. how many bits we use for AD conversion.

QKS output consists of:

1) a C function K (controller) which takes the AD-converted values for the system state and outputs the commands to be sent first to the DA (Digital-to-Analog) conversion and then to the plant actuators. The guaranteed WCET (Worst Case Execution Time) of such a function is also output, so that it is possible to check if real-time requirements are satisfied. If the AD function is simple enough, also the C code for AD is generated.

2) a C function exists_K (controllable region) which takes the AD-converted values for the system state and outputs 1 if it is controllable by K, and 0 otherwise. Note that all states in the controllable region are guaranteed to be correctly driven to the goal.

3) Gnuplot input files which may be used in order to obtain a visual representation of the controllable region.

Please note that QKS rests on an incomplete algorithm, since the problem being addressed (that is, the DTLHS quantized control problem) is undecidable. Accordingly, upon termination QKS also returns one of the following results:

Sol) meaning that the generated control software is able to drive any state in the desired controllable region towards the goal;

NoSol) meaning that there cannot exist a control software able to drive any state in the desired controllable region towards the goal;

Unk) meaning that the generated control software is not able to drive any state in the desired controllable region towards the goal (i.e., the output controllable region is strictly contained in the input desired controllable region), but a control software achieving this objective may exist.

The bitbucket page for QKS is here

The current version of QKS may be downloaded here.