Modelling and verification of evolving cyber-physical spaces

Computing and communication capabilities are increasingly being embedded into physical spaces thus blurring the boundary between computational and physical worlds; typically, this is the case in modern cyber-physical systems, like smart buildings or smart cities. Conceptually, such composite environments, hereafter called cyber-physical spaces (CPSp), can be abstracted into a topological model where computational and physical entities are connected in a discrete, graph-like structure. Like any other software-intensive system, a CPSp is highly dynamic and typically undergoes continuous change, a fact we emphasise by the notion of evolving CPSp. This brings a manifold of challenges as dynamics may affect safety, security, or reliability requirements of the overall space-dependent software system. Formally modelling space and its dynamics as well as supporting reasoning about various properties of evolving space, is a crucial prerequisite for engineering dependable evolving CPSp, e.g. to assure requirements satisfaction or to trigger correct adaptation. Thus, we propose a methodology and technical framework which support modelling of evolving cyber-physical spaces and reasoning about their spatio-temporal properties. We utilise bigraphs as a formalism for modelling CPSp 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 feature adopting logic-based specification of properties and according model checking procedures, in both spatial and temporal fragments. Utilising these foundations, we consider systematically engineering systems and support both verification of requirements in early stages of design and devising adaptive security behaviours at run time.

La separazione tra mondo fisico ed elettronico è in costante riduzione. Dispositivi con capacità computazionale sono sempre maggiormente presenti negli spazi fisici riducendo le barriere tra uomo e macchina. Tipicamente, questo avviene nei moderni sistemi cyber-fisici, come smart building e city. Questi ambienti, indicati nel seguito come spazi cyber-fisici (CPSp), possono essere astratti mediante modelli topologici, dove entità computazionali e fisiche sono connesse per mezzo di strutture matematiche, come ad esempio grafi. Come tutti i sistemi software, gli spazi cyber-fisici sono estremamente dinamici e tipicamente sono soggetti a continui cambiamenti. Questa costante evoluzione comporta una serie di sfide riguardanti la sicurezza e l’affidabilità del sistema. Modellizzare formalmente lo spazio nel quale un’applicazione è in esecuzione e la sua evoluzione, fornendo dei meccanismi che consentano di ragionare sulle proprietà del sistema a fronte dei vari cambia- menti, è un prerequisito essenziale per progettare degli spazi cyber-fisici che soddisfino i loro requisiti a fronte dei cambiamenti che avvengono nello spazio. Questa tesi propone una metodologia e un framework che supportano la modellizzazione di un sistema cyber-fisico e della sua evoluzione e l’analisi delle sue proprietà spazio-temporali. Vengono utilizzati bigraph come formalismo per modellizzare i CPSp e i suoi cambiamenti. Il sistema così generato è un sistema reattivo specificato per mezzo di regole di riscrittura che modellizzano l’evoluzione del sistema in base a condizioni che possono verificarsi localmente e globalmente nel sistema. Il meccanismo di reasoning consente di selezionare le funzionalità del sistema utilizzando un algoritmo di model checking per verificare il soddisfacimento di un insieme di requisiti specificati per mezzo di appropriati formalismi logici. La metodologia proposta consente di progettare un sistema, consentendo la modifica dei meccanismi di sicurezza a run time e la verifica dei requisiti del sistema durante tutto il processo di design.