Information Technology Reference
In-Depth Information
2.
A
proof technique
teasing apart aspects of the monitor correctness definition, Lem. 3,
Lem. 4 and Lem. 5, allowing us to prove correctness in stages. We subsequently ap-
ply this technique to prove the
correctness of our tool
,Thm.2.
3.
An alternative
violation
characterisation of the logic, sHML, that is more amenable
to runtime analysis and reasoning about monitor correctness, together with a proof
of correspondence for this reformulation, Thm. 1.
4.
An extension of a formalisation for Erlang describing its tracing semantics, Sec. 2.
5.
A formal monitor synthesis definition from sHML formulas to Erlang code, Def. 6.
Related Work:
The aforementioned work, [17,27,4], discusses monitor synthesis from a
di
erent logic, namely LTL, to either pseudocode, automata or Buchi automata; none of
this work considers online concurrent monitoring, circumventing issues associated with
concurrency and system interference. There is considerable work on runtime monitor-
ing of web services, e.g., [13,5] verifying the correctness of reactive (communication)
properties, similar to those expressed through sHML; to the best of our knowledge, none
of this work tackles correct monitor synthesis from a specified logic. In [9], Colombo
et al. develop an Erlang RV tool using the EVM tracing mechanism but do not con-
sider the issue of correct monitor generation. Fredlund [16] adapted a variant of HML
to specify correctness properties in Erlang, albeit for model checking purposes. There
is also work relating HML formulas with tests, namely [1]. Our monitors di
ff
er from
tests, as in [1], in a number of ways: (
i
) they are defined in terms of
concurrent
actors,
as opposed to
sequential
CCS processes; (
ii
) they analyse systems
asynchronously
, act-
ing on traces, whereas tests interact with the system
directly
, forcing certain system
behaviour; (
iii
) they are expected to
always
detect violations when they occur whereas
tests are only required to have
one
possible execution that detects violations.
ff
Future Work:
The monitoring semantics of Section 2 can be used as a basis to formally
prove existing Erlang monitoring tools such as [9,10]. sHML can also be extended to
handle limited, monitorable forms of liveness properties (often termed co-safety prop-
erties [21]). It is also worth exploring mechanisms for synchronous monitoring, as op-
posed to asynchronous variant studied in this paper. Erlang also facilitates monitor
dis-
tribution
which can be used to lower monitoring overheads [11]. Distributed monitoring
can also be used to increase the expressivity of our tool so as to handle correctness prop-
erties for distributed programs. The latter extension, however, poses a departure from
our setting because the unique trace described by our framework would be replaced by
separate independent traces at each location, where the lack of a total ordering of events
may prohibit the detection of certain violations [14].
References
1. Aceto, L., Ingolfsdottir, A.: Testing Hennessy-Milner Logic with Recursion. In: Thomas, W.
(ed.) FOSSACS 1999. LNCS, vol. 1578, pp. 41-55. Springer, Heidelberg (1999)
2. Armstrong, J.: Programming Erlang. The Pragmatic Bookshelf (2007)
3. Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Ro¸u, G., Sokolsky,
O., Tillmann, N. (eds.): RV 2010. LNCS, vol. 6418. Springer, Heidelberg (2010)
