Simulink model
Important!
Our model can be downloaded here:- Plasma project: PigsShed.plasma
- Simulink models:
- Base model: cochons.slx
- Model without failures: cochons_nofail.slx
- Optimized model (without scopes): cochons_optim.slx
To execute the model you will need to build the S-Function Builder in Simulink:
- Right click on S-Function Builder block and select “Properties”
- Launch “Build”
The system under control is a pig shed equipped with a fan and a heater to regulate the air temperature. Air temperature in the shed is subjected to random variations due to the variation of external temperature and the variation of the number of pigs that produce heat. The objective of the controller is to counter these variations such that the temperature remains within a given comfort zone. To do so, the controller can activate the heater to increase the temperature, and the fan to bring external air and therefore cool the shed. Then the temperature T of the shed is given by the following differential equation:
where is the external temperature, is the air flow created by a minimal flow , and an additional flow when the fan is activated, is the heat produced by the heater, when activated, and is the heat produced by the pigs. This equation is modeled by the following Simulink subsystem:
The number of pigs is determined every 500 time units according to a Poisson law with . The external temperature is modulated by two sinusoidal between and , with periods 628 t.u and 62.8 t.u.
The controller that we study applies a bang-bang strategy that is specified by four threshold:
- When the temperature goes above , the fan is turned on.
- When the temperature returns below , the fan is turned off.
- When the temperature goes below , the heater is turned on.
- When the temperature returns above , the heater is turned off.
This controller is implemented by the following Stateflow automata:
The fan and the heater are subjected to random failures when they are in used. Exponential distributions control the occurrence time of a failure. After a failure a reparation process allows to restart the fan or the heater, but it also takes a random time, exponentially distributed. These failures are modelled by two Stateflow automata:
In this automaton, is a random number between 0 and 1, and is the duration of use of the fan or heater. The timings and corresponds respectively to the time of next failure, and the repaire time, each chosen according to an exponantial distribution with parameter and , respectively.
Verification
The controller objective is to maintain the temperature within a comfort zone specified by a minimum and a maximun temperature (resp. and ). In this section we consider the following values for the controller thresholds: , , and .We apply statistical model-checking to evaluate the efficiency of the controller both in the presence and absence of failures.
The first BLTL property that we monitor checks that the system is not in discomfort for an excessive period of time. This is expressed by the following property:
where is the simulation time, is the accepted discomfort time, and is a predicate that is true when the temperature of the system is outside the comfort zone.
A second BLTL property checks that each period of discomfort is followed by a period without discomfort:
Here and are as previously, while is the expected time at which the system returns to normal situation and is the duration of the period without discomfort.
We use PlasmaLab statistical model-checker to estimate the probability to satisfy these properties for different values of the timing constraints. Each property is evaluated over a period of time with 100 simulations. is evaluated for several values of and is evaluated with and and several values of .
Without failure | With failures | ||
0.87 0.99 1.0 |
0.01 0.23 0.78 |
||
0.95 0.9 |
0.57 0.08 |
Optimisation
We want to optimise the performances of the system such that it minimizes the discomfort and the energy cost spent in heating and cooling. To achieve this we can manipulates the 4 temperature thresholds of the controller. Each threshold is therefore assigned to a range of values. The product of these values gives a set of initial conditions to analyse the system. PlasmaLab can evaluate the values of the cost and the discomfort for each of these values. We can then select the best values of the parameters according to the pareto curve: