Information Technology Reference
In-Depth Information
the network is always linked to the specification, and proves, with the previous dy-
namic monitoring process theory [7], that the introduction of interruptible blocks to the
syntax and semantics yields a sound theory. The proofs can be found in [35].
ε
→
∗
Δ
Theorem 1 (Session fidelity).
If
Δ
corresponds to G
1
,...,
G
n
and
Δ
0
,
,
Σ
,there
Σ
→
∗
Δ
,
Δ
corresponds to G
1
,...,
G
n
which are derivatives of
exists
Δ
,
ε
such that
G
1
,...,
G
n
.
5.2
Related Work
Distributed Runtime Verification.
The work in [3] explores runtime monitoring based
on session types as a test framework for multi-agent systems (MAS). A global session
type is specified as cyclic Prolog terms in Jason (a MAS development platform). Their
global types are less expressive in comparison with the language presented in this paper
(due to restricted arity on forks and the lack of session interrupts). Their monitor is
centralised (thus no projection facilities are discussed), and neither formalisation, global
safety property nor proof of correctness is given in [3].
Other works, notably from the multi-agent community, have studied distributed en-
forcement of global properties through monitoring. A distributed architecture for local
enforcement of global laws is presented by Zhang et al. [36], where monitors enforce
laws
expressed as event-condition-action. In [26], monitors may trigger sanctions if
agents do not fulfil their obligations within given deadlines. Unlike such frameworks,
where all agents belonging to a group obey the same set of laws, our approach asks
agents to follow personalised laws based on the role they play in each session.
In runtime verification for Web services, the works [24,25] propose FSM-based mon-
itoring using a rule-based declarative language for specifications. These systems typi-
cally position monitors to protect the safety of service interfaces, but do not aim to
enforce global network properties. Cambronero et al. [8] transform a subset of Web Ser-
vices Choreography Description Language into timed-automata and prove their trans-
formation is correct with respect to timed traces. Their approach is model-based, static
and centralised, and does not treat either the runtime verification or interrupts. Baresi et
al. [5] develop a runtime monitoring tool for BPEL with assertions. A major difference
is that BPEL approaches do not treat or prove global safety. BPEL is expressive, but
does not support distribution and is designed to work in a centralised manner. Kruger et
al. [22] propose a runtime monitoring framework, projecting MSCs to FSM-based dis-
tributed monitors. They use aspect-oriented programming techniques to inject monitors
into the implementation of the components. Our outline monitoring verifies conversa-
tion protocols and does not require such monitoring-specific augmentation of programs.
Gan [14] follows a similar but centralised approach of [22]. As a language for proto-
col specification, a main advantage of Scribble (i.e. MPST) over alternatives, such as
message sequence charts (MSC), CDL and BPML, is that MPST has both a formal ba-
sis and an in-built mechanism (projection) for decentralisation, and is easily integrated
with the language framework as demonstrated for Python in this paper.
Language-Based Monitoring Tools.
Jass [19] is a precompiler tool for monitoring
the dynamic behaviour of sequential objects and the ordering of method invocations
