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.
Specifying and verifying real-time self-adaptive systems / M. Camilli, A. Gargantini, P. Scandurra - In: Software Reliability Engineering (ISSRE), 2015 IEEE 26th International Symposium onPrima edizione. - [s.l] : IEEE, 2015 Nov. - ISBN 9781509004058. - pp. 303-313 (( Intervento presentato al 26. convegno ISSRE tenutosi a Gaithersburg nel 2015 [10.1109/ISSRE.2015.7381823].
Specifying and verifying real-time self-adaptive systems
M. Camilli
Primo
;P. ScandurraUltimo
2015
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.File | Dimensione | Formato | |
---|---|---|---|
07381823.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
207.52 kB
Formato
Adobe PDF
|
207.52 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.