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

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.