AUTOMATION IN BUILDINGS AND FORMAL METHODS

The paper presents a case study based on our practical model of energy saving in a small building equipped by an industrial distributed control system. First, we overview our model built over LonWorks networking platform and then we discuss increasing the reliability of control programs by formal methods. Their possible application is demonstrated by the example of verifying the control program for a solar space heating. We show that some safety verifications are performable without constructing a whole hybrid model. Finally, we discuss the results achieved up to date.The principles presented in this case study are applicable on a general level for other similar systems.