ABSTRACT
The chapter presents the related work on security in the smart home domain and justifies the choice of Discrete Controller Synthesis (DCS) over other formal techniques to provide a solution for the controllability problem. It describes the synchronous framework which serves as a foundation for modeling and applying DCS. The chapter explains how to define a smart home model using this synchronous framework. It shows the application of DCS on such a model. The chapter details the experiments the conducted, using a partial model of our own smart home equipment. The model is kept partial so that both DCS application and controller execution remain easy to follow step by step. From the various smart home presentations found in the related work, a smart home system for people with disabilities can be abstracted as a hierarchy of hardware and software components, sensors and effectors distributed among several interconnected rooms, helping a person with impairments to perform activities of daily living.
