Computer systems are invading our homes and take over tedious tasks. The manually operated valve on radiators first became the mechanical thermostat, and is now becoming a computerised smart thermostat that not only keeps the room at a certain temperature, but also detects and predicts occupancy to improve efficiency and environmental impact. The modern refrigerator no longer has a scale between one to five, but is set to an exact temperature and is about to be connected to the Internet, such that surplus of electricity from photovoltaic panels and wind turbines can be stored as ice in the freezer.
Almost needless to say, this have resulted in an increasing demand for new technologies. Not only do appliances become smarter, but also they connect in networks to utilise the advantages of collaboration. Collaboration both within the home itself, but also with the external world. To cope with the complexity of this new world, researchers propose models and model checking tools to ensure continued dependability of the developed solutions.
This thesis presents our work on connecting model tools with gateways, with the purpose of easing development and test of these new systems, being it just prototype benches or real occupied homes. In total three toolchains and a method are presented; the first is essentially an interpreter for Uppaal models, the second executes Event-Condition-Action (ECA) rules, and the third finds the optimal strategy for a floor heating system. It is common for them all that they allow models to control hardware directly without the need for manual translation to code. The work describes how feature interactions can be found systematically and is thus the first step towards integrating detection for these in the toolchains. These toolchains generally performs well and help test models in practice, but the work shows that there there are still some remaining issues and limitations to be investigated in further work.
All interested parties are welcome. After the defense the department will be hosting a small reception in cluster 1.