Information Technology Reference
In-Depth Information
clarify the aspects of a certain domain. One example of the latter is AADL, the
Architectural Analysis and Design Language [28]. For many of these languages
the work is considered done once the syntax is fixed, and an intuitive explana-
tion of the semantics is provided. Formalizing these intuitions is sometimes a
task for legions of scientists: The conception of Statecharts for instance has lead
to several dozens of different semantics, and more are on the horizon. Still, one
of the lessons generally learnt from these experiences is that a good semantics
is compositional [29], a semantics that provides a meaning to an object based
on a composition of the semantics of its parts. If the composition adheres to
simple-to-grasp rules, this semantics can become consensus. Compositionality is
a fundamental and highly desirable property of a semantics: it enables compo-
sitional reasoning, i.e. analyzing complex systems by breaking them down into
their constituting parts. Examples
par excellence
of simple-to-grasp rules have
been given before: parallel composition and hiding.
A clean and well-understood semantics is a necessity for model-based evalua-
tion of such languages. It is as simple as that. Whenever performance figures or
correctness claims are presented for UML fragments or the like, they are specific
to the semantics chosen, and in case that semantics is neither commonly agreed
nor easy-to-grasp, doubts remain concerning the general validity of such claims.
Dynamic fault trees.
Let us consider a classical domain specific language, known
as fault trees. Fault trees were first planted in the youth of civil nuclear energy,
as means to systematically quantify the risk of a catastrophic hazard [63] in a
plant. A fault tree is a diagrammatical variation of a boolean function, drawn
in a tree-structured manner where the leaves correspond to boolean variables.
These leaves represent basic operational units of the plant such as valves and
pipes. The failure of an operational components flips the corresponding boolean
value to true. If the entire function evaluates to true, a catastrophic event is
supposed to be unavoidable. Fault trees have been standardised, and their use is
prescribed in many engineering areas. A classical fault tree is static, the order of
failure occurences is assumed not important, and components cannot be replaced
dynamically by spare components. If considering such extensions, one arrives at
the diagrammatical notation of dynamic fault trees (DFT) [25].
The semantics of a dynamic fault tree can no longer be mapped directly on
a boolean function, but instead needs a state-transition graph representation to
reflect the system dynamics. If one assumes that failure occurences follow expo-
nential laws, which is a standard and sometimes justified assumption, it seems
natural to expect that the resulting model is a CTMC. Actually, the first com-
plete formalisation attempted [21] aimed at providing a CTMC semantics, but
revealed a number of ambiguities in the DFT framework. Most notably, in some
instances of DFTs non-determinism arises. This is where IMC and its composi-
tionality property can play a pivotal role: The work of Crouzen
et al.
[12,11,10]
provides a clean and elegant compositional semantics, a semantics that maps on
IMC. More precisely, the semantics takes up ideas of I/O-automata [53], and
uses
input/output
interactive Markov chains (I/O-IMC). I/O-IMC are restricted
versions of IMC that allow for non-blocking communication. The semantics is
