Smart Environments (SmE) are a growing combination of various computing frameworks (ubiquitous, pervasive etc), devices, control algorithms and a complex web of interactions. It is at the core of user facilitation in a number of industrial, domestic and public areas. Based on their application areas, SmE may be critical in terms of correctness, reliability, safety, security etc. To achieve error-free and requirement-compliant implementation, these systems are designed resorting to various modeling approaches including Ontology and Statecharts. This paper attempts to consider correctness, reliability, safety and security in the design process of SmE and its related components by proposing a design time modeling and formal verification methodology. The proposed methodology covers various design features related to modeling and formal verification SmE (focusing on users, devices, environment, control algorithms and their interaction) against the set of the requirements through model checking. A realistic case study of a Bank Door Security Booth System (BDSB) is tested. The results show the successful verification of the properties related to the safety, security and desired reliable behavior of BDSB.
Modeling and Formal Verification of Smart Environments / Corno, Fulvio; Sanaullah, Muhammad. - In: SECURITY AND COMMUNICATION NETWORKS. - ISSN 1939-0122. - STAMPA. - 7:10(2014), pp. 1582-1598. [10.1002/sec.794]
Modeling and Formal Verification of Smart Environments
CORNO, Fulvio;SANAULLAH, MUHAMMAD
2014
Abstract
Smart Environments (SmE) are a growing combination of various computing frameworks (ubiquitous, pervasive etc), devices, control algorithms and a complex web of interactions. It is at the core of user facilitation in a number of industrial, domestic and public areas. Based on their application areas, SmE may be critical in terms of correctness, reliability, safety, security etc. To achieve error-free and requirement-compliant implementation, these systems are designed resorting to various modeling approaches including Ontology and Statecharts. This paper attempts to consider correctness, reliability, safety and security in the design process of SmE and its related components by proposing a design time modeling and formal verification methodology. The proposed methodology covers various design features related to modeling and formal verification SmE (focusing on users, devices, environment, control algorithms and their interaction) against the set of the requirements through model checking. A realistic case study of a Bank Door Security Booth System (BDSB) is tested. The results show the successful verification of the properties related to the safety, security and desired reliable behavior of BDSB.File | Dimensione | Formato | |
---|---|---|---|
UserModeling.pdf
accesso aperto
Tipologia:
2. Post-print / Author's Accepted Manuscript
Licenza:
PUBBLICO - Tutti i diritti riservati
Dimensione
1.81 MB
Formato
Adobe PDF
|
1.81 MB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
https://hdl.handle.net/11583/2506415
Attenzione
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo