A tool generates online monitor for perturbed STL

We demonstrate the simulation results of the benchmark using a HVAC Simulink model.

1. Physical model. In this part, we build the temperature and humidity dynamics which are influenced by outside environment , human, radiators and air conditioning.

2. Controller. To control vectorial signal, so we use Switch block rather than StateFlow to implement the control logic. User can change this module with ML component as demand.

3. Environment. It is worth noting that Environment is the stochastic part of the entire model including the outdoor environment and people influence on temperature which the number of people is parameterized. Weather datas are extrapolated to fit our need from the dataset https://www.kaggle.com/selfishgene/historical-hourly-weather-data.

4. Evaluations. This part is for verification about HVAC system.

We present three properties relative to thermal comfort. We set Tim to 1 and the property is specified by the formula !φ.

With the help of our tool SOMPS, online monitors are constructed as shown in below. For formula φ, we set Tim to 1 and use a sinusoidal block for the airflow to highlight perturbation more. We get the online monitor structure in Fig. 11(c) and Fig. 11(d).