Detecting and Resolving Feature Interactions in Cyber-Physical Systems Using Formal Methods

We investigate the use of formal methods to detect and resolve feature interactions (FI) in cyber-physical systems (CPS). These systems are often made up of multiple components that may interact with each other in unexpected and unwanted ways, potentially creating a security risk. Specifically, we use supervisory control theory to examine FI in a smart home, an example of a CPS. With the rising adoption of smart home devices, mitigating these interaction threats at the modelling stage is important before they are installed in homes. We present an extended taxonomy of FI threats that affect such a CPS. We demonstrate how one such threat, chaotic device management (Codema), can be detected and resolved in a system comprised of a smart light bulb that supports two disjointed device management channels.