On the Runtime Enforcement of Timed Properties - CORSE - Computer Optimization and Run-time SystEms Accéder directement au contenu
Chapitre D'ouvrage Année : 2019

On the Runtime Enforcement of Timed Properties

Résumé

Runtime enforcement refers to the theories, techniques, and tools for enforcing correct behavior of systems at runtime. We are interested in such behaviors described by specifications that feature timing constraints formalized in what is generally referred to as timed properties. This tutorial presents a gentle introduction to runtime enforcement (of timed properties). First, we present a taxonomy of the main principles and concepts involved in runtime enforcement. Then, we give a brief overview of a line of research on theoretical runtime enforcement where timed properties are described by timed automata and feature uncontrollable events. Then, we mention some tools capable of runtime enforcement, and we present the TiPEX tool dedicated to timed properties. Finally, we present some open challenges and avenues for future work. Runtime Enforcement (RE) is a discipline of computer science concerned with enforcing the expected behavior of a system at runtime. Runtime enforcement extends the traditional runtime verification [12-14, 42, 43] problem by dealing with the situations where the system deviates from its expected behavior. While runtime verification monitors are execution observers, runtime enforcers are execution modifiers. Foundations for runtime enforcement were pioneered by Schneider in [98] and by Rinard in [95] for the specific case of real-time systems. There are several tutorials and overviews on runtime enforcement for untimed systems [39, 47, 59], but none on the enforcement of timed properties (for real-time systems). In this tutorial, we focus on runtime enforcing behavior described by a timed property. Timed properties account for physical time. They allow expressing constraints on the time that should elapse between (sequences of) events, which is useful for real-time systems when specifying timing constraints between statements, their scheduling policies, the completion of tasks, etc [5, 7, 88, 101, 102]. This tutorial comprises four stages: 1. the presentation of a taxonomy of concepts and principles in RE (Sec. 1); 2. the presentation of a framework for the RE of timed properties where specifications are described by timed automata (preliminary concepts are recalled in Sec. 2, the framework is overviewed in Sec. 3, and presented in more details in Sec. 4); 3. the demonstration of the TiPEX [82] tool implementing the framework (Sec. 5); 4. the description of some avenues for future work (Sec. 6).
Fichier principal
Vignette du fichier
rv19-tutorial.pdf (1012.98 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02433521 , version 1 (09-01-2020)

Identifiants

Citer

Yliès Falcone, Srinivas Pinisetty. On the Runtime Enforcement of Timed Properties. Proceedings of the Runtime Verification 2019 conference, Springer, pp.48-69, 2019, ⟨10.1007/978-3-030-32079-9_4⟩. ⟨hal-02433521⟩
104 Consultations
194 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More