Please use this identifier to cite or link to this item:
Title: Synthesising correct concurrent runtime monitors
Authors: Francalanza, Adrian
Seychell, Aldrin
Keywords: Autonomous distributed systems
Computer network architectures
Formal methods (Computer science)
Computer software -- Development
Computer software -- Verification
Aspect-oriented programming
Computer software -- Testing
ERLANG (Computer program language)
Issue Date: 2015
Publisher: Springer New York LLC
Citation: Francalanza, A., & Seychell, A. (2015). Synthesising correct concurrent runtime monitors. Formal Methods in System Design, 46(3), 226-261.
Abstract: This paper studies the correctness of automated synthesis for concurrent monitors. We adapt a subset of the Hennessy-Milner logic with recursion (a reformulation of the modal μ-calculus) to specify safety properties for Erlang programs. We also define an automated translation from formulas in this sub-logic to concurrent Erlang monitors that detect formula violations at runtime. Subsequently, we formalise a novel definition for monitor correctness that incorporates monitor behaviour when instrumented with the program being monitored. Finally, we devise a sound technique that allows us to prove monitor correctness in stages; this technique is used to prove the correctness of our automated monitor synthesis.
Appears in Collections:Scholarly Works - FacICTCS

Files in This Item:
File Description SizeFormat 
rv13jour.pdf253.19 kBAdobe PDFView/Open

Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.