System Description

The Concentration Control System Example

System Description

The CheckMate model example called Concentration Control System (CCS) is comprised of three tanks: Tank 1 stores an alkaline solution, Tank 2 an acid solution, and Tank 3 receives material from both tanks to form a product. CCS is used to control the concentration of a certain ingredient for a batch operation. For our purpose, the concentration is measured indirectly from the pH level in Tank 3. The two continuous state variables of interest are the level (x1) and the concentration (pH) of the product (x2) in Tank 3. For this system, it has to be guaranteed that the concentration in Tank 3 satisfies 6.8 < x2 < 7.2 when the batch is finished (Tank 3 is full, x1=1.0 m). The initial condition is x2=7.1 and x1=0. In normal operation, the Tank 3 is filled with product and the controller has to monitor the pH-value making sure it is within [6.8,7.2]. If x2 >= 7.2, the controller adds acid solution from Tank 2, driving the pH-value again to the normal region. If x2 <= 6.8, the controller adds alkaline solution from Tank 1 to correct the pH-value back into the desired interval. An overview of the physical system that the model represents is shown below.

image001
Overview of CCS CheckMate example.

System Requirements

The requirements for the CCS can be stated as follows:  “for all possible initial conditions, the pH level is normal at the time when the Tank 3 is full, in the end of the batch”. In other words, when Tank 3 is full (x1 >1), a sample is taken and the process ends successfully if 6.8 < x2 < 7.2, Otherwise, the process failed.   If we call avoid the discrete state of the system when Tank 3 is full and the pH is not normal, and call reach the discrete state when Tank 3 is full and pH is normal, we can state the property to be investigated as follows: the proposition avoid should be false for all possible trajectories of the CCS and the proposition reach is true at least once in each trajectory. CheckMate automatically tests the system for this particular specification if the user names a discrete state in the CheckMate model "avoid".  See the user guide for instructions on creating CheckMate models.

Simulink Model

In constructing a CheckMate model for the purposes of analysis, we may first wish to implement the system as a general Simulink model, or we may be given a general Simulink model of a system and wish to construct a CheckMate model.  This section describes how this might be done for the CCS. 

The first step in modeling any system is identifying the important dynamics.  In the case of the CCS the important dynamics can be summarized as follows:

The CCS can be modeled using standard MATLAB/Simulink blocks, as shown below. To run it, first run the file setup_ph_plant.m and then type the name of the MDL file ph_plant_sim.mdl.

image018
Simulink implementation of CCS.

To simplify the explanation the Simulink model was drawn using four colors, blue, yellow, green and orange. The model are described below:

Below we show a typical trajectory generated by the Simulink model, where level is in the X axis and pH is in the Y axis. We can see that the pH oscillates until Tank 3 is full. For this case, the pH is normal when the batch ends.

image018
Simulation of CCS Simulink model.

In constructing the Simulink model of the system we have identified several things:

Hybrid Automaton Model

The CCS can be formally modeled as a hybrid system.  A hybrid automaton that models the CCS is shown below.

image033
Hybrid automaton for the pH plant system.

Note that the system dynamics only can change when there are transitions between discrete states. The initial discrete state is Normal pH and continuous initial state is 0< x1 <  0.1 and 7.05 < x2 < 7.15.   To perform the test whether or not the specification is satisfied, the user can define two Tank full states. One is Tank full when the system was in normal operation and the other Tank full when the system where in Low pH or High pH.   Since this is a change for verification purposes, it will be included only in the CheckMate model.  

CheckMate Model

Below, the CCS example is implemented using the CheckMate   frontend.  It uses the MATLAB/Simulink GUI. There are three customized special blocks as follows: Switched Continuous System Block (SCSB), drawn in blue; Polyhedral Threshold Blocks (PTHB's), drawn in green, and the StateFlow   Machine block (SFMB), drawn in yellow.

image036
CheckMate model for the CCS.

The SCSB

The SCSB represents the continuous dynamics of the system.  It takes inputs from a Stateflow block that determine what discrete state the system is in and if a reset has occurred.  Double-clicking on the SCSB reveals a list of alterable parameters.  For the pH plant example, these parameters convey the following information:

image040
Information for the SCSB tank.

It is interesting to observe that the function executed by the blue blocks of the Simulink model (built before) are the ones being replaced by the SCSB tank. For example, the switching between the dynamics of x1 was done using two values correcting_pH_level_dynamics and   normal_level_dynamics.   Each one of these correspond to a mode selected inside SCSB.

CheckMate provides the ability to define parameters for certain elements in the modeling that change over a range of values. For the CCS, the concentration increasing can be given as a parameter. The default value for simulation is given in an additional field in the SCSB template. The range in which the parameter will vary is given as a linear-constraint-object called PH_PAR, for the CCS example. Below is the template for the case where we have parameters.

image042
Information for the SCSB tank, including parametric information.

The PTHB

The PTHB's take inputs from the output of the SCSB, which is the state of the system.  The PTHB's point to linearcons that represent polyhedra that are used to build guard regions.  When the state of the system enters the linearcon, the output of the PTHB (a boolean) goes from false to true (zero to one).  The definitions for the linearcons that the PTHB's point to can be found in 'setup_ph.m'. For the pH plant example, there are   four PTHB's used for the CCS example:   phnormal (x2<7.0); highph (x2>7.2); lowph (x2<6.8) and tankfull (x1>1).   All the green blocks in the MATLAB/Simulink diagram (Shown before) are replaced by the PTHB, because their function were to trigger transitions.

image044
PTHB block.

The StateFlow Block

This block describes the system's discrete-state switching logic.  It takes boolean inputs from the PTHB's.  Each state is given a name and assigned a unique, integer 'q' value.  This 'q' value is output to the SCSB.  For the CCS example, there are four states: normal, alkaline, acid,   avoid, and reach.  The system starts in normal and evolves continuously until a transition to alkaline, acid or reach happens. From alkaline state, the system can either go back to normal or go to avoid, if the event full happens. For the acid state, , the system can either go back to normal or go to avoid, if the event full happens. The states reach and avoid are terminal states, meaning that there is no outgoing transitions from them.

image046
StateFlow Block.

Building the CheckMate model

All CheckMate models must contain the components described in the previous section.  An SCSB must be present in order to implement the system’s continuous dynamics.  The continuous dynamics must serve as input to the PTHB’s, which generate a boolean output for Stateflow blocks.

User-defined files

CheckMate requires several user-defined m files in order to perform analysis.  Among other things, these m files specify continuous state system dynamics, system specifications, the polyhedral regions used for the PTHB’s, and numerical parameters. For the CCS system, the user files are as follows:

The 'setup_ph.m' File

This file contains the definitions of the linearcon objects used by the   PTHB's (i.e. regions used to create guards for the system) and also used for the initial continuous set, and the analysis region. For example, the linearcon that represents the Tank 3 full is defined as:

tankfull =linearcon([],[], [-1 0],-1);

This command creates a linearcon with one inequality (one half-space).  Specifically, this inequality is -x2£-1or x2>1. 

Also, the setup file contains the system specification.  This is a computation-tree-logic (CTL) expression that the routines explore and verify use to analyze the system (see the documentation files for pointers to papers that introduce CTL).

The 'ph_function.m' File

This file contains the description of the continuous-time dynamics for the CCS example.  The function returns the right-hand-side of the differential equation.  The dynamics change depending on the current discrete state of the system.  For example, when the system is in discrete location 1 (u=1), the system evolves by way of linear dynamics. The other dynamics follow the hybrid automaton description. The states reach and avoid both represent the state Tank full, for the case when the pH is inside the specification limits and outside, respectively. The CCS has no reset function associated. In the ph_function.m file there is no reference to resets.

The 'ph_param.m'

This file contains all of the numerical parameters necessary to perform verification.   See the documentation for a description of these parameters.

Simulation

Pressing the "play" button on the Simulink window can simulate the CCS.  The initial conditions specified inside the SCSB will be used as initial conditions for the continuous variables.  Simulating the system with the default initial conditions will produce the following result inside the XY plot scope.

image052
StateFlow Block.

Explore

The command explore tests whether or not the system specification holds for various simulation runs.    It tests the fulfillment/violation of a specification for sets of single trajectories.  With the pH model open, type "explore" at the command line.  A simulation will automatically run with the initial conditions set to the value found in the SCSB block in the model.  CheckMate will discover that the specification (of not terminating the batch outside the normal levels) holds for this simulation run.  We provided the specification in the setup_ph.m file. CheckMate automatically identifies if the user named any states in the StateFlow diagram by the names reach; or avoid.

The output will look like the following:

>>explore

block orders: x = [tank], q = [controller], pth = [highph lowph phnormal tankfull]

init:

c:\matlab6.1\checkmate3.0\demo\ph_plant\ph_plant

t = 0.0001, x = [0 7.1], q = 1, pth = [0 0 0 0]

  ---> ... --> terminal / specification satisfied

>>

The output of explore tells the user what specification was being test, the initial state of the system, the value of the output of the PTHB's at the initial instant, and that the specification was satisfied. In this case, we provided the specification in the setup_ph.m file. CheckMate automatically identifies if the user named any states in the StateFlow diagram by the names reach; or avoid.

For the CCS, the SFMB has both names, what makes the program to investigate these two expressions, when performing explore and verify commands. The additional output for the explore command is as follows:

computing specification 1 of 2 in the list

block orders: x = [tank], q = [controller], pth = [highph lowph phnormal tankfull]

init:

c:\matlab6.1\checkmate3.0\demo\ph_plant\ph_plant

t = 0.0001, x = [0 7.1], q = 1, pth = [0 0 0 0]

  ---> ... --> terminal

For initial condition x = [0 7.1]: The system never enters the state "avoid"

  / specification satisfied

  computing specification 3 of 3 in the list

block orders: x = [tank], q = [controller], pth = [highph lowph phnormal tankfull]

init:

c:\matlab6.1\checkmate3.0\demo\ph_plant\ph_plant

t = 0.0001, x = [0 7.1], q = 1, pth = [0 0 0 0]

  ---> ... --> terminal

For initial condition x = [0 7.1]: The system enters the state "reach".

The command explore can be used also for the vertices of the initial condition set. For the CCS, if the user types:

>> explore -vertices

This explore option will take the vertices of the PH_ICS   linearcon and use them as initial conditions for simulation.  Explore then tests if the specification holds for each simulation point.  If the parametric version is used, it will also check for the vertices of the linearcon that composes the parametric space (PH_PAR for the CCS system).

Finally, explore also can be used for a particular set of point using the following option:

>> a=[0.3 ; 7.15];

>> explore -points a

This will cause the analysis to explore the trajectories starting from the points x=[0.3; 7.15]

 

Verification

Simulation and exploration give the user some preliminary information about the behavior of the system. On the other hand, if the specification has to be checked for all possible trajectories, starting at some initial set, a formal verification analysis is necessary. After opening the  CCS model, the user can invoke the verification using the following command:

>> verify

verify has several arguments that the user can apply to change the way the verification is done, when to stop, how to save information, etc. the command verify creates several data structures. The most important ones are GLOBAL_PIHA, GLOBAL_AUTOMATON and GLOBAL_TRANSITION. For details about these structures for this particular example, there is the command “document”. For details type help document in the MATLAB prompt.

Next figure shows the reachable states for the verification of the CCS example (with no parametric information). The verification failed because there is one case where the pH =7.2 when the Tank 3 is full. This is a hard situation to simulate using MATLAB, just because depending on the way the simulation model is built the event full will come before event highph, and the second one will not be received. This is one example where the verification can tell us information that it is not obvious if we just simulate the system.

image052
Reachable states for CCS.

If the verification fails, the program asks the user if a refinement is desired. Roughly speaking, the refinement consists in splitting the state space in smaller pieces, connecting the pieces where there is a possibility for a discrete transition and checking the specification against the new transition system.