Modelling and Verification of Safety of Access Control in SCADA Systems.

Modern safety-critical systems become increasingly networked and interconnected. To ensure their safety, the designers should guarantee not only that the critical parameters are accessed and modified by authorised users and components but also that the permitted operations should not violate safety. Traditionally, the designers rely on Role-Based Access Control (RBAC) to define the access to the system parameters. In this paper, we define a safety-aware RBAC model that takes into account current system state and safety of intended actions. Our approach relies on contract-based reasoning and formal modelling in Event-B. The approach is illustrated by a case study - a supervised control of a power switch.