Synthesising Correct Concurrent Runtime Monitors - Runtime Verification - page 112

Synthesising Correct
Concurrent Runtime Monitors
(Extended Abstract)

Adrian Francalanza and Aldrin Seychell

Computer Science, ICT, University of Malta
{ afra1,asey0001 } @um.edu.mt

Abstract. We study the correctness of automated synthesis for concurrent mon-
itors. We adapt sHML, a subset of the Hennessy-Milner logic with recursion, to
specify safety properties of Erlang programs, and define an automated transla-
tion from sHML formulas to Erlang monitors so as to detect formula violations
at runtime. We then formalise monitor correctness for our concurrent setting and
describe a technique that allows us to prove monitor correctness in stages; this
technique is used to prove the correctness of our automated monitor synthesis.

Keywords: runtime verification, monitor synthesis, concurrency, actors, Erlang.

1 Introduction

Runtime Verification (RV) [3], is a lightweight verification technique for determining
whether the current system run observes a correctness property. Two requirements are
crucial for the adoption of this technique. First, runtime monitor overheads need to be
kept to a minimum so as not to degrade system performance. Second, instrumented
monitors need to form part of the trusted computing base of a system by adhering
to an agreed notion of monitor correctness ; amongst other things, this normally in-
cludes a guarantee that runtime checking corresponds (in some sense) to the property
being checked for. Monitor overheads and correctness are occasionally conflicting con-
cerns. For instance, in order to lower monitoring overheads, engineers increasingly use
concurrent monitors [11,22,28] so as to exploit better the underlying parallel and dis-
tributed architectures pervasive to today's computers. However concurrent monitors are
also more susceptible to elusive errors such as non-deterministic monitor behaviour,
deadlocks or livelocks which may, in turn, a

ect their correctness.
Ensuring monitor correctness is non-trivial. One prominent obstacle is the fact that
system properties are typically specified using one formalism, e.g., a high-level logic,
whereas the respective monitors checking these properties are described using another
formalism, e.g.,a programming language—this makes it hard to ascertain the semantic
correspondence between the two descriptions. Automated monitor synthesis can miti-
gate this problem by standardising the translation from the property logic to the monitor
formalism. It also gives more scope for a formal treatment of monitor correctness.
In this work, we investigate the correctness of synthesised monitors in a concur-
rent setting , whereby ( i ) the system executes concurrently with the synthesised monitor

ff