View Proposal

---

Proposer

Rob Stewart

Title

Model checking Home Assistant automation rules

Goal

Apply LTL model checking to validate Home Assistant automation rules

Description

Home Assistant is widely used open source home automation software. It allows users to set up automation rules, with triggers based on many things, including sensor readings (person detection) and time (after 6pm). These rules can be expressed as YAML files, or using the Home Assistant GUI, or using a 3rd party tool GUI like Node-RED. They typically have (1) a trigger, (2) optional additional preconditions, and (3) an action. For large home automations, a user may have Home Assistant dozens if not hundreds of automation rules. These can contradict each other (turn a light on when someone enters the room and turn light off when someone enters the room), or cause race conditions (if light off then turn on and if light on then turn off). Sometimes they are quite subtle race conditions, e.g. turn light on when luminescence is low and turn light off when luminescence is high because the light bulbs emits light which alters the luminescence. This project will explore the use of model checking to validate home automation rules. The model checker will check for consistency across and contradictions across all rules. If there is time, a very neat use case of this model checking approach would be to simplify the set of home automation rules while preserving the intended automation behaviours.

Resources

Background

Url

External Link

Difficulty Level

Moderate

Ethical Approval

Full

Number Of Students

1

Supervisor

Rob Stewart

Keywords

Degrees