Analysis of energy-efficient buildings through simulation and formal methods

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.