A Formal Verification Analysis of a Bayesian Inference-Based Sensors and Actuators Control System

Formal verification of a control system relies on the ability to construct a finite state transition model from a set of logical rules. An efficient search procedure can check whether a desired system property holds true in that model under perturbations of system parameters and disturbances. Formal verification methods provide full coverage of all possible cases (scenarios), and thereby check whether the specified system properties are satisfied. This paper describes the application of formal verification techniques to improve the performance of an office temperature sensors and actuators control system. The control system model is expressed in the form of if..then rules. These rules were extracted by a Bayesian inference engine from statistical data for a real-life case. We verified the office temperature control system properties with the help of RuleBase, a formal verification tool developed by the IBM Haifa Research Laboratory. We analyzed the rule set and showed how the rules can be updated. We also checked the robustness of the control strategy. Our results show that formal verification techniques are capable of finding control parameters for an inference rule-based model of a sensors and actuators control system