This paper reports on the use of a method to encourage the use of formal verification to explore the correctness of the development of an Ambient Assisted Living system, in this case one to help people with asthma to better manage their condition. We apply the methodology by modelling in ProMeLa and using SPIN for simulation and verification. We illustrate how the method is applied and some of the insights the developing team gained in its application.