Tsigkanos, ChristosKehrer, TimoGhezzi, CarloTichy, MatthiasBodden, EricKuhrmann, MarcoWagner, StefanSteghöfer, Jan-Philipp2019-03-292019-03-292018978-3-88579-673-2https://dl.gi.de/handle/20.500.12116/21180In this work, we report about recent research results on the Modeling and Verification of Evolving Cyber-Physical Spaces, published in ESEC/FSE17. We increasingly live in cyber-physical spaces – spaces that are both physical and digital, and where the two aspects are intertwined. Such spaces are highly dynamic and typically undergo continuous change. Software engineering can have a profound impact in this domain, by defining suitable modeling and specification notations as well as supporting design-time formal verification. In this paper, we present a methodology and a technical framework which support modeling of evolving cyber-physical spaces and reasoning about their spatio-temporal properties. We utilize a discrete, graph-based formalism for modeling cyber-physical spaces as well as primitives of change, giving rise to a reactive system consisting of rewriting rules with both local and global application conditions. Formal reasoning facilities are implemented adopting logic-based specification of properties and according model checking procedures, in both spatial and temporal fragments. We evaluate our approach using a case study of a disaster scenario in a smart city.enCyber-Physical SpacesDependable Software-Intensive SystemsSafety and ReliabilityModelling and SpecificationFormal VerificationText/Conference Paper1617-5468