A BRS-based Modeling Approach for Secure Medical Cyber-Physical Systems

This last decade, Medical Cyber-Physical Systems (M-CPS) have emerged to enable smart healthcare systems to monitor, process and make autonomous decisions without the need to involve doctors and other users. However, M-CPS pose several challenges, the security of medical devices being one of the most critical ones. To deal with these issues, formal reasoning facilities will undoubtedly have a profound impact in this context. In this paper, we present an iterative process which supports design and modeling of any CPS in general, as well as the analysis and the reasoning about its dynamic and secure behavior. In the main phase of this process, we utilize CA-BRS (Control Agent and Bigraphical Reactive System) model, an extension of BRS formalism to deal with physical and virtual aspects of CPS, and GTR (Guided Transitions System), a state space definition to specify dynamic and adaptive behavior of safe and secure CPS. To ensure security and safety of M-CPS, we apply our formalization approach to represent the structural aspect of M-CPS, consisting of physical or cyber entities in which agents of CA-BRS are hosting, and their complex behavior aspect. By modeling the interactions and behaviors of individual agents, through a set of controlled reaction rules, emergent properties can arise at a higher level, which may not be immediately predictable from the behavior of individual agents alone.