Please use this identifier to cite or link to this item:
https://www.um.edu.mt/library/oar/handle/123456789/86002
Title: | On bidirectional runtime enforcement |
Other Titles: | Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2021. Lecture Notes in Computer Science, vol 12719 |
Authors: | Aceto, Luca Cassar, Ian Francalanza, Adrian Ingólfsdóttir, Anna |
Keywords: | Software engineering Computer software -- Verification Computer logic Object monitors (Computer software) Recursive functions -- Data processing |
Issue Date: | 2021 |
Publisher: | Springer |
Citation: | Aceto, L., Cassar, I., Francalanza, A., & Ingólfsdóttir, A. (2021). On bidirectional runtime enforcement. 41st IFIP WG 6.1 International Conference, FORTE 2021, Valletta. 3-21. |
Abstract: | Runtime enforcement is a dynamic analysis technique that instruments a monitor with a system in order to ensure its correctness as specified by some property. This paper explores bidirectional enforcement strategies for properties describing the input and output behaviour of a system. We develop an operational framework for bidirectional enforcement and use it to study the enforceability of the safety fragment of Hennessy-Milner logic with recursion (sHML). We provide an automated synthesis function that generates correct monitors from sHML formulas, and show that this logic is enforceable via a specific type of bidirectional enforcement monitors called action disabling monitors. |
URI: | https://www.um.edu.mt/library/oar/handle/123456789/86002 |
Appears in Collections: | Scholarly Works - FacICTCS |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
On Bidirectional Runtime Enforcement.pdf Restricted Access | 563.37 kB | Adobe PDF | View/Open Request a copy |
Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.