Abstract
Self-adaptive systems autonomously adapt their behavior at run-time to react to internal dynamics and to uncertain and changing
environment conditions. Specification and verification of self-adaptive systems are generally very difficult to carry out
due to their high complexity, especially when involving time constraints. In the last case, in fact, the correctness of systems
depends also on the time associated with events. This paper introduces a formal approach to specify and verify the self-adaptive
behavior of real-time systems. Our specification formalism is based on Time-Basic Petri nets, a particular timed extension
of Petri nets. We propose adaptation models to realize self-adaptation with temporal constraints and we adopt a zone-based
modeling approach to support separation of concerns during the modeling phase. Zones identified during the modeling phase
can be then used as modules (TB Petri subnets) either in isolation, to verify intra-zone properties, or all together, to verify
inter-zone properties over the entire system model and check that all the temporal deadlines are met. We illustrate our approach
by modeling and verifying a time-critical Gas Burner system that exhibits a self-healing behavior.
[download the pdf file] [DOI]