Instrumenting Runtime Enforcement
Hublet, François Basin, David Hu, Linda Krstić, Srđan Reese, Lennard
Hublet, François
Basin, David
Hu, Linda
Krstić, Srđan
Reese, Lennard
Supervisor
Department
Computer Science
Embargo End Date
Type
Conference proceeding
Date
License
Language
Collections
Research Projects
Organizational Units
Journal Issue
Abstract
Runtime enforcement ensures that a running system complies with a property by observing and modifying the system’s actions. In practice, the property is often defined in terms of high-level, abstract events, while the system’s behavior consists of low-level, concrete actions. The relationship between actions and events is established in the instrumentation process, where developers must ensure that (i) system actions report the right events, and (ii) the necessary modifications to the system’s behavior are correctly enforced. However, the abstraction gap between a high-level property and low-level actions makes this process error-prone.In this paper, we refine an existing formal model of runtime enforcement, which leaves instrumentation implicit, into a more precise model that explicitly accounts for instrumentation. We propose a correctness criterion for instrumentation and present a novel library, called InstrLib, that instruments Python applications for runtime enforcement.
Citation
F. Hublet, D. Basin, L. Hu, S. Krstić, L. Reese, "Instrumenting Runtime Enforcement," 2025, pp. 160-180.
Source
Lecture Notes in Computer Science
Conference
International Conference on Runtime Verification
Keywords
46 Information and Computing Sciences, 4612 Software Engineering
Subjects
Source
International Conference on Runtime Verification
Publisher
Springer Nature