Model verification techniques, such as model checking, generally require relatively advanced expertise. They are therefore typically used in applications where their usefulness is especially appreciated, if not necessary, and can ofset their costs. Critical system design has, for instance, been one of the main consumers of such techniques. They could however bring benefits to many other domains. Development times can be shortened by the drastically reduced number of mistakes in verified design models. Moreover, they can help reduce the number of bugs remaining in shipped products. Lowering barriers to entry for the application of these techniques should therefore have a significant impact. In this work, we show how model checking can be applied to UML models in the smart home context. The models were created with AnimUML, which makes them markedly easier to create than with traditional tools. Furthermore, this tool's direct model analysis support at the UML level makes it relatively simple to verify properties. It was able to detect several corner case issues, which would have been much harder to detect, and especially diagnose, with testing only. Besides being time consuming, testing reaches its fundamental limits, checking what the system should not do. Besides, in the home automation context, the problem is even more complex due to the distributed nature of the problem [1]. The situation can certainly be improved by using formal verification approaches, like model-checking. These techniques, naturally geared towards distributed systems, allow the verification of properties expressing what the system should do, which naturally completes the correctness specification of a system. During the last decade, tremendous progress was achieved on this axis [2, 3], however most of the proposed approaches and tools require a high-degree of sophistication from the home automation designer. Moreover, the marketing target of home automation solutions, like Google Smart Home1, is wide and targets non-expert users. Nevertheless, the modeling community started a push towards lively verification environments [ 4], which enables seamless user interaction during the design and debugging process. The AnimUML environment [5, 6, 7] pushes the frontiers of this approach by allowing not only early debugging of high-level specifications, but also
formal verification of partial (under development) specifications. This work presents a case study2 where a LYWSD03MMC3 temperature and humidity sensor is integrated with the Google Smart Home automation platform using local fulfillment 4. We leverage the capabilities ofered by AnimUML both to better understand the overall architecture, through lively user-model interactions, and to allow for the verification of non-trivial properties. The two main limitations of the approach are the following. 1) Although the tooling significantly helps, it is still necessary to learn to use AnimUML. 2) In addition to modeling the app, the designer must also model the behavior of the Smart Home API, and of the device. Regarding the first issue, we plan to keep improving the tool to make it easier to learn and use. As for the second issue, ideally manufacturers should provide such models. Moreover, we already provide a reusable Google Smart Home API model as part of our case study. 2Case study material is available on GitHub at https://github.com/fjouault/SmartHomeCaseStudy. 3https://esphome.io/components/sensor/xiaomi_ble.html#lywsd03mmc 4https://developers.google.com/assistant/smarthome/concepts/local