On Dependable Cyber-Physical Spaces of Critical Infrastructures

In modern societies, people live in spaces populated by a variety of computational elements, which generate new kinds of active cyber-entities interacting with each other and with humans, enabling new smart functionalities. Examples range from smart buildings such as modern office spaces, hospitals, airports and other public facilities up to entire smart cities. Such systems in which cyber and physical entities, particularly humans, are interacting in space may be collectively indicated as cyber-physical spaces (CPSp’s). Many of these systems are part of critical infrastructures, and thus dependability in its various notions is a fundamental concern in their design and operation. To that end, the design of CPSp’s should focus on dependability requirements since the early development stage, through modelling and continuous verification, until operation, where monitoring and run-time verification techniques ensure that the system complies with the requirements, even in the presence of possible changes and unforeseen system evolution. We argue that a holistic approach to achieve dependability of CPSp’s must be founded on a formal specification of the requirements, on formal models of the system exposing well-defined semantics, and on automatic verification procedures which span the entire lifecycle from design to run-time. In this chapter, we illustrate the general approach which we are developing in our research and show how it can be instantiated and used in a case study reflecting a generalized operational environment of a critical facility.