Self-adaptive software systems are able to autonomously adapt their behavior at run-time to react to internal dynamics and to uncertain and changing environment conditions. Formal specification and verification of self-adaptive systems are tasks generally very difficult to carry out, especially when involving time constraints. In this case, in fact, the system correctness depends also on the time associated with events. This article introduces the Zone-based Time Basic Petri nets specification formalism. The formalism adopts timed adaptation models to specify self-adaptive behavior with temporal constraints, and relies on a zone-based modeling approach to support separation of concerns. Zones identified during the modeling phase can be then used as modules either in isolation, to verify intra-zone properties, or all together, to verify inter-zone properties over the entire system. In addition, the framework allows the verification of (timed) robustness properties to guarantee self-healing capabilities when higher levels of reliability and availability are required to the system, especially when dealing with time-critical systems. This article presents also the ZAFETY tool, a JAVA software implementation of the proposed framework, and the validation and experimental results obtained in modeling and verifying two time-critical self-adaptive systems: the Gas Burner system and the Unmanned Aerial Vehicle system.
(2018). Zone-based formal specification and timing analysis of real-time self-adaptive systems [journal article - articolo]. In SCIENCE OF COMPUTER PROGRAMMING. Retrieved from http://hdl.handle.net/10446/131457
Zone-based formal specification and timing analysis of real-time self-adaptive systems
Camilli, Matteo;Gargantini, Angelo;Scandurra, Patrizia
2018-01-01
Abstract
Self-adaptive software systems are able to autonomously adapt their behavior at run-time to react to internal dynamics and to uncertain and changing environment conditions. Formal specification and verification of self-adaptive systems are tasks generally very difficult to carry out, especially when involving time constraints. In this case, in fact, the system correctness depends also on the time associated with events. This article introduces the Zone-based Time Basic Petri nets specification formalism. The formalism adopts timed adaptation models to specify self-adaptive behavior with temporal constraints, and relies on a zone-based modeling approach to support separation of concerns. Zones identified during the modeling phase can be then used as modules either in isolation, to verify intra-zone properties, or all together, to verify inter-zone properties over the entire system. In addition, the framework allows the verification of (timed) robustness properties to guarantee self-healing capabilities when higher levels of reliability and availability are required to the system, especially when dealing with time-critical systems. This article presents also the ZAFETY tool, a JAVA software implementation of the proposed framework, and the validation and experimental results obtained in modeling and verifying two time-critical self-adaptive systems: the Gas Burner system and the Unmanned Aerial Vehicle system.File | Dimensione del file | Formato | |
---|---|---|---|
scp-17.pdf
accesso aperto
Versione:
draft - bozza non referata
Licenza:
Licenza default Aisberg
Dimensione del file
1.97 MB
Formato
Adobe PDF
|
1.97 MB | Adobe PDF | Visualizza/Apri |
1-s2.0-S0167642318300753-main.pdf
Solo gestori di archivio
Versione:
publisher's version - versione editoriale
Licenza:
Licenza default Aisberg
Dimensione del file
2.64 MB
Formato
Adobe PDF
|
2.64 MB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
Aisberg ©2008 Servizi bibliotecari, Università degli studi di Bergamo | Terms of use/Condizioni di utilizzo