Information Technology Reference
In-Depth Information
by annotating Java programs with specifications that can be checked at runtime. Other
approaches to runtime verification of program execution by monitors generated from
language-based specifications include: aspect-oriented programming [23]; other works
that use process calculi formalisms, such as CSP [19]; monitors based on FSM skeletons
associated to various forms of underlying patterns [1,4]; and the analysis of dynamic
parametric traces [4]. Our monitor framework has been influenced by these works and
shares similarities with some of the presented RV techniques. However, the target pro-
gram domain and focus of our work are different. Our framework is specifically de-
signed for decentralised monitoring of distributed programs with diverse participants
and interleaving sessions, as opposed to monitoring the execution of a single program
and verifying its local properties. The basis of our design and implementation is the
theory of multiparty session types, over which we have developed practically motivated
extensions to the type language and the methodology for runtime verification.
6Con lu ion
We have implemented the first dynamic verification of distributed communications
based on multiparty session types and shown that a new feature for interruptible con-
versations is effective in the runtime verification of message exchanges in a large cy-
berinfrastructure [28] and Web services [33,34]. Our implementation automates dis-
tributed monitoring by generating FSMs from local protocol projections. We sketched
the formalisation of asynchronous interruptions with conversation scopes, and proved
the correctness of our design through the session fidelity theorem. Future work includes
the incorporation of more elaborate handling of error cases into monitors and automatic
generation of service code stubs. Although our implementation work is ongoing through
industry collaborations, the results already confirm the feasibility of our approach. We
believe this work contributes towards methodologies for better specification and more
rigorous governance of network conversations in distributed systems.
Acknowledgements.
We thank Gary Brown and the Scribble team for discussions and
collaborations. This work has been partially sponsored by the Ocean Observatories Ini-
tiative, VMWare, Cognizant and EPSRC EP/K034413/1, EP/K011715/1, EP/G015635/1
and EP/G015481/1.
References
1. Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhotak, O., de Moor,
O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to
aspectj. SIGPLAN Not 40(10), 345-364 (2005)
2. Advanced Message Queuing protocols (AMQP) homepage,
http://jira.amqp.org/
3. Ancona, D., Drossopoulou, S., Mascardi, V.: Automatic generation of self-monitoring mass
from multiparty global session types in Jason. In: Baldoni, M., Dennis, L., Mascardi, V., Vas-
concelos, W. (eds.) DALT 2012. LNCS, vol. 7784, pp. 76-95. Springer, Heidelberg (2013)
4. Avgustinov,
P., Tibble,
J., de
Moor,
O.: Making
trace
monitors
feasible. SIGPLAN
Not 42(10), 589-608 (2007)
