• A synthesis tool for optimal m...

Treffer: A synthesis tool for optimal monitors in a branching-time setting ; Coordination models and languages COORDINATION 2022

Title:
A synthesis tool for optimal monitors in a branching-time setting ; Coordination models and languages COORDINATION 2022
Authors:
Achilleos, Antonis, Exibard, Leo, Francalanza, Adrian, Lehtinen, Karoliina, Xuereb, Jasmine
Publisher Information:
Springer Nature Switzerland AG
Publication Year:
2022
Collection:
University of Malta: OAR@UM / L-Università ta' Malta
Subject Terms:
Computer programs -- Verification, Modality (Logic), Calculus -- Computer programs, System analysis -- Computer programs, Formal methods (Computer science)
Document Type:
Konferenz conference object
Language:
English
Relation:
https://www.um.edu.mt/library/oar/handle/123456789/131353
DOI:
10.1007/978-3-031-08143-9_11
Availability:
https://www.um.edu.mt/library/oar/handle/123456789/131353
https://doi.org/10.1007/978-3-031-08143-9_11
Rights:
info:eu-repo/semantics/restrictedAccess ; The copyright of this work belongs to the author(s)/publisher. The rights of this work are as defined by the appropriate Copyright Legislation or as modified by any successive legislation. Users may access this work and can make use of the information contained in accordance with the Copyright Legislation provided that the author must be properly acknowledged. Further distribution or reproduction in any format is prohibited without the prior permission of the copyright holder.
Accession Number:
edsbas.20874C43
Database:
BASE

Weitere Informationen

Monitorability is a characteristic that delineates between the properties that can be runtime verified by a monitor and those that cannot. Existing notions of monitorability for branching-time specifications are quite restrictive, limiting the set of monitorable properties to a small logical fragment. A recent study has enlarged the set of monitorable branching-time properties by weakening the requirements expected of the monitors effecting the verification: it defines a novel notion of optimal monitor that carries out the maximum number of detections that can be effected for any property, thereby turning a branching-time property into a monitorable one. The study also outlines a method for obtaining a unique optimal monitor from any branching-time property but falls short of providing an automation for this procedure. In this paper, we present a prototype tool that generates monitorable properties for branchingtime properties expressed in a variant of the modal μ-calculus, based on this procedure. We also assess the performance of the prototype tool by evaluating its performance against several specifications. ; peer-reviewed