Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
We acknowledge that the construction of such a probabilistic model constitutes a separate and significant research problem [4].
- 2.
For convenience, the formal definition of an MDP is applied to the context of our problem setting, ignoring rewards and the discount factor. We assume that the effects of any action taken in a particular state depend only on that state and not on the prior history.
References
Barkowsky, T., Bateman, J.A., Freksa, C., Burgard, W., Knauff, M.: Transregional collaborative research center SFB/TR 8 spatial cognition: reasoning, action, interaction. it–Inf. Technol. 47(3), 163–171 (2005)
Birkedal, L., Damgaard, T.C., Glenstrup, A.J., Milner, R.: Matching of bigraphs. Electron. Notes Theor. Comput. Sci. 175(4), 3–19 (2007)
Bivand, R.S., Pebesma, E., Gómez-Rubio, V.: Spatial Data Import and Export. Springer, Berlin (2013)
Busari, S.A., Letier, E.: Radar: A lightweight tool for requirements and architecture decision analysis. In: Proceedings of the 39th International Conference on Software Engineering, pp. 552–562. IEEE Press, Piscataway (2017)
Calinescu, R., Ghezzi, C., Kwiatkowska, M.Z., Mirandola, R.: Self-adaptive software needs quantitative verification at runtime. Commun. ACM 55(9), 69–77 (2012)
Ciancia, V., Latella, D., Loreti, M., Massink, M.: Specifying and verifying properties of space. In: Theoretical Computer Science, pp. 222–235. Springer, Berlin (2014)
Ciancia, V., Grilletti, G., Latella, D., Loreti, M., Massink, M.: An experimental spatio-temporal model checker. In: International Conference on Software Engineering and Formal Methods, pp. 297–311. Springer, Berlin (2015)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Conforti, G., Macedonio, D., Sassone, V.: Spatial Logics for Bigraphs. Springer, Berlin (2005)
Corradini, A., Montanari, U., Rossi, F., Ehrig, H., Heckel, R., Löwe, M.: Algebraic approaches to graph transformation-part I: Basic concepts and double pushout approach. In: Handbook of Graph Grammars, pp. 163–246. University of Pisa, Pisa (1997)
Day, M.: The move to BIM with archicad 12. In: AEC Magazine. August 23, 2008
Eastman, C., Eastman, C.M., Teicholz, P., Sacks, R.: BIM Handbook: A Guide to Building Information Modeling for Owners, Managers, Designers, Engineers and Contractors. Wiley, Hoboken (2011)
Egenhofer, M.J., Frank, A.U., Jackson, J.P.: A Topological Data Model for Spatial Databases. Springer, Berlin (1989)
Egenhofer, M.J., Herring, J.: Categorizing binary topological relations between regions, lines, and points in geographic databases. The 9, 94–1 (1990)
Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Formal Methods for Eternal Networked Software Systems, pp. 53–113. Springer, Berlin (2011)
Gadducci, F., Heckel, R., Koch, M.: A fully abstract model for graph-interpreted temporal logic. In: International Workshop on Theory and Application of Graph Transformations, pp. 310–322. Springer, Berlin (1998)
Gianni, D., Bocciarelli, P., D’Ambrogio, A., Iazeolla, G.: A model-driven and simulation-based method to analyze building evacuation plans. In: Proceedings of the 2015 Winter Simulation Conference, pp. 2644–2655. IEEE Press, Piscataway (2015)
Greenyer, J., Gritzner, D., Gutjahr, T., König, F., Glade, N., Marron, A., Katz, G.: Scenariotools–a tool suite for the scenario-based modeling and analysis of reactive systems. Sci. Comput. Program. 149, 15–27 (2017)
Hamacher, H.W., Tjandra, S.A.: Mathematical Modelling of Evacuation Problems: A State of Art. Fraunhofer-Institut (ITWM), Munich (2001)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Asp. Comput. 6(5), 512–535 (1994)
Isikdag, U., Underwood, J., Aouad, G.: An investigation into the applicability of building information models in geospatial environment in support of site selection and fire response management processes. Adv. Eng. Inform. 22(4), 504–519 (2008)
ISO 16739: Industry Foundation Classes (IFC): Data Sharing in the Construction and Facility Management Industries (2013)
Aufaure-Portier, M.-A., Trépied, C.: A survey of query languages for geographic information systems. In: Proceedings of the 3rd International Workshop on Interfaces to Databases, pp. 1–14, Napier University, Edinburgh (1996)
Milner, R.: The Space and Motion of Communicating Agents. Cambridge University Press, Cambridge (2009)
Perrone, G., Debois, S., Hildebrandt, T.T.: A Verification Environment for Bigraphs. Innov. Syst. Softw. Eng. 9(2), 95–104 (2013)
Porter, S., Tan, T., Tan, T., West, G.: Breaking into BIM: Performing static and dynamic security analysis with the aid of BIM. Autom. Constr. 40, 84–95 (2014)
Sevegnani, M., Calder, M.: Bigraphs with sharing. Theor. Comput. Sci. 577, 43–73 (2015)
Sevegnani, M., Unsworth, C., Calder, M.: A SAT Based Algorithm for the Matching Problem in Bigraphs with Sharing. Technical Report, University of Glasgow (2010)
Tsigkanos, C., Pasquale, L., Ghezzi, C., Nuseibeh, B.: On the interplay between cyber and physical spaces for adaptive security. IEEE Trans. Dependable Secure Computing PP(99), 1–1 (2016)
Tsigkanos, C., Kehrer, T., Ghezzi, C.: Architecting dynamic cyber-physical spaces. Computing 98(10), 1011–1040 (2016)
Tsigkanos, C., Kehrer, T., Ghezzi, C.: Modeling and verification of evolving cyber-physical spaces. In: Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2017, pp. 38–48 (2017)
Zhang, S., Teizer, J., Lee, J.K., Eastman, C.M., Venugopal, M.: Building information modeling (BIM) and safety: automatic safety checking of construction models and schedules. Autom. Constr. 29, 183–195 (2013)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Kehrer, T., Tsigkanos, C., Ghezzi, C. (2020). On Dependable Cyber-Physical Spaces of Critical Infrastructures. In: Keupp, M. (eds) The Security of Critical Infrastructures. International Series in Operations Research & Management Science, vol 288. Springer, Cham. https://doi.org/10.1007/978-3-030-41826-7_10
Download citation
DOI: https://doi.org/10.1007/978-3-030-41826-7_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-41825-0
Online ISBN: 978-3-030-41826-7
eBook Packages: Business and ManagementBusiness and Management (R0)