This paper describes a formal approach to modelling and verification of self-adaptive real-time systems. Such systems can dynamically be affected by exception events either originated in the operational environment or in the internal status, which require to be dealt with through adaptation actions which have to fulfil timing constraints. The approach is based on Time Basic (TB) Petri nets, a formalism well-suited to the specification of time-critical systems. Although some special-case tools have been developed to support the analysis of TB net models, the original contribution of this paper is an embedding of TB nets into the popular Uppaal toolbox based on timed automata, which makes it possible both non-deterministic exhaustive analysis by model checking and/or a quantitative analysis of model properties through statistical model checking. The paper demonstrates the application of TB net modelling and analysis through a self-healing time-critical system.

Formal Modelling and Verification of Real-Time Self-Adaptive Systems

Franco Cicirelli
Membro del Collaboration Group
;
Libero Nigro
Membro del Collaboration Group
;
Francesco Pupo
Membro del Collaboration Group
2019-01-01

Abstract

This paper describes a formal approach to modelling and verification of self-adaptive real-time systems. Such systems can dynamically be affected by exception events either originated in the operational environment or in the internal status, which require to be dealt with through adaptation actions which have to fulfil timing constraints. The approach is based on Time Basic (TB) Petri nets, a formalism well-suited to the specification of time-critical systems. Although some special-case tools have been developed to support the analysis of TB net models, the original contribution of this paper is an embedding of TB nets into the popular Uppaal toolbox based on timed automata, which makes it possible both non-deterministic exhaustive analysis by model checking and/or a quantitative analysis of model properties through statistical model checking. The paper demonstrates the application of TB net modelling and analysis through a self-healing time-critical system.
2019
Modelling and verification, self-adaptive systems, real time, timing constraints, Time Basic Petri nets, model checking, statistical model checking, Uppaal
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.11770/295155
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 1
social impact