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 speci?cation and veri?cation of self-adaptive systems are tasks generally
very di?cult 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 speci?cation 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 identi?ed 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 veri?cation 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.
[download the pdf file] [DOI]