Analysis of Energy-Efficient Buildings through Simulation and Formal Methods

Abstract

In the last few years, the increasing interest in energy saving has led to invest resources in many research fields, in order to develop new technologies to reduce energy consumption. One such field is energy management systems for buildings. The interactions between the system controlling the building and its environment are complicated by the fact that they involve important timing properties, which can be expressed through a variety of formalisms. This paper introduces a formal model, expressed in a temporal logic language, through which designers can evaluate the temporal behavior of buildings' energy management systems. To this end, the formal model is analyzed through simulation, that is, through the generation of traces satisfying the temporal logic model.

Keywords

• Data analysis
• Energy efficient
• Formal methods

-

Managing the technology that is used to control the various functions of modern buildings is a complex task. The U.S. Department of Energy estimates that buildings in industrialized countries account for around 40% of total energy consumption. Researchers have shown that savings in the order of 20-30% can be gained through careful energy management and control in buildings, even without changing the structure of the hardware configuration of their energy supply systems[ 1 ]. The problem of modeling and designing software control systems has been approached through different techniques, such as temporal logic languages[ 2 ], which are supported by a wide range of techniques for model analysis and verification. This work aims to introduce a solution for describing the management and control of energy consumption in buildings through rules expressed in temporal logic. The architecture of the approach is described through a simple example, namely the control of Rooms provided with various appliances. The rest of the paper is organized as follows. Section 2 introduces the simulation tools on which the approach is founded; Section 3 introduces the temporal logic language used for describing control rules; and Section 4 illustrates the case study which exemplifies the main characteristics of the proposed analysis method based on temporal logic rules. Section 5 concludes. The Appendix shows an example of execution trace produced through the Zot tool, which is used in this work to simulate temporal logic models. 2 2.1

Tool support

OpenModelica A number of well-established techniques have been developed over the years to model physical phenomena, which constitute the environment of software systems. Typically, these phenomena are described through a continuous notion of time, using approaches that can be classified as either causal or acausal. In causal approaches, the model is decomposed into blocks which interact through input and output variables. The objectoriented language Modelica [ 3 ], instead, follows a acausalapproach where each (physical) component is specified through a system of differential algebraic equations; connections between modules, which correspond to physical principles, are set by equating effort variables and by balancing flow variables. OpenModelica1 is an open-source simulation engine based on the Modelica language; it can be interfaced with the Zot tool described below to create closed-loop simulations of software systems and their environments [ 4 ]. 2.2

Zot Zot2can perform formal verification of models described through temporal logic formulae. More precisely, let us call S the model of the designed system, which corresponds to a set of temporal logic formulae. If S is input to the Zot tool, the latter looks for an execution trace of the modelled system; that is, for each time instant and for each predicate appearing in the formulae of S, it looks for an assignment of values which make the formulae of S true. If no such trace is found (i.e., if the model is unsatisfiable), then the model is contradictory, meaning that it contains some flaw that makes it unrealizable in practice. 1http://openmodelica.org 2github.org/fm-polimi/zot

The TRIO temporal logic language

In this section we provide a brief overview of the temporal logic, called TRIO [ 1 ], which has been used in this work to capture the rules governing the energy management system. TRIO allows users to express timing properties of systems, including real-time ones. TRIO adopts a linear notion of time, and can be used to express properties over both discrete and continuous temporal domains. Table 1 presents some typical TRIO temporal operators, which are defined in terms of the basic Dist operator, where Dist(φ, d) means that formula φ holds at the instant exactly d time units from the current one.

Case Study: Rooms with Appliances

In this section we briefly describe how the energy management system is captured through the TRIO temporal logic language. In particular, we focus on an example of building whose rooms are provided with appliances whose energy consumption needs to be controlled. The model of the building is fed to the Zot tool to generate traces, which can then be analyzed to unearth anomalous behaviors. Fig. 1. shows the corresponding Modelica diagram describing the structure and the components of the analyzed system. The appliances considered are: 1. the Electric Boiler, whose desired temperature is 70°C; 2. the Washer whose desired temperature is 60°C and whose washing cycle lasts an hour;3. The Bath, which can be used both as shower or as a bath; 4. The Oven, whose nominal power consumption is 1000W; 5. The DishWasher, whose washing cycle is an hour and a half; 6. The Refrigerator, whose nominal power consumption is 90W;7. The HoodCookTop and the Stove, which are used when a user cooks with the stove and keeps the hood turned on.

These appliances are connected through three different networks: the hydraulic, the thermal, and the electric network.

In the rest of this section, we present the formulae capturing the behavior of the appliances. For the Electric Boiler, if the water temperature is less than 70°C for 2 minutes, then the boiler is turned on (represented by predicate boilerOn being true):

Alw(Lasted(boiler_water_temp< boiler_desired_temp, 2)⇒boilerOn). If the water temperature is higher than 70°C for 2 minutes, then the controller is turned off (i.e., “not boilerOn” holds):

Alw(Lasted(boiler_water_temp> boiler_desired_temp, 2)⇒ ¬boilerOn). The following formula constrains the difference between the current temperature and the one at the next minute when the boilers turned on; in particular, the temperature must increase (i.e., the difference is greater than 0), but by no more than 2 degrees (i.e., the difference is less than 3).

Alw(boilerOn ⇒next(boiler_water_temp) - boiler_water_temp> 0 ∧ next(boiler_water_temp) - boiler_water_temp< 3) Also after the boiler is turned off, the temperature decreases by with a rate of at most 2 degrees per minute: Alw(¬boilerOn ⇒ next(boiler_water_temp) - boiler_water_temp<1∧ next(boiler_water_temp) - boiler_water_temp>-3) The following formula constrains the range of the temperature to be between -20°C and 100°C: Alw(boiler_water_temp< 101 ∧ boiler_water_temp> -20)  Washer: The time washing cycle lasts60 min:

Alw(washer_start⇔Futr(washer_end, 60)) The washer is on between a “start” and an “end” command.

Alw(washer_on⇔Sinceei(¬washer_end, washer_start)

The washer cannot start again until the current cycle has finished.

Alw(washer_start⇒Untilei(¬washer_start, washer_end)  Dryer : The model of the dryer is very similar to the one of the washer.

The time spin/dryer cycle is 30 min. Alw(dryer_start⇔ Futr(dryer_end,30))

The dryer is on between a “start” and an “end” command.

Alw(dryer_on ⇔ Sinceei(¬dryer_end, dryer_start) The dryer cannot not start again until the current cycle has finished.

Alw(dryer_start ⇒ Untilei(¬dryer_start, dryer_end)  Oven : If the door of the oven is opened for 2 minutes, the controller is on (i.e., it flashes):

Alw(Lasted(oven_door_open, 2) ⇒oven_door_flash)  Dishwasher :  Refrigerator : The model of the dishwasher is also very similar to the one of the washer and of the dryer. The model of the refrigerator is similar to the one for the oven; that is, if the refrigerator door is opened for 2 minutes, the controller is on (i.e., it flashes). 5

Conclusion

This paper introduces imulation-based mechanisms based on rules formalized in temporal logic, which can help improve the user’s understanding of modeled systems. The proposed approach can be used to model (complex) systems and describe their properties formally; it allows the user to simulate the behavior of the system and verify the satisfiability of the properties of interest. We exemplified our approach on a case study concerning the modeling of an energy management system for a building.

Appendix: Example of execution trace of the model

References

1. Guian .X , Xu . Z , Jia .Q : Energy efficient building facilitated by micro grid . IEEE Power and Energy Society General Meetings , 2010 .

2. Furia , C. , Mandrioli , D. , Morzenti , A. , Rossi , M : Modelling Time in computing . SpringerVerlag , 2012 .

3. Fritzson .P.: Principles of object-oriented modeling and simulation with Modelica 2.1 . John Wiley and Sons, 2004 .

4. Baresi , L. , Ferretti , G. , Leva , A. , Rossi , M : Flexible logic-basedco-simulation of Modelica models . In: IEEE InternationalConference on Industrial Informatics (INDIN) ,pp. 635 - 640 ( 2012 )