Model-based runtime analysis of distributed reactive systems [Elektronische Ressource] / Andreas Klaus Bauer

Sujets

• Informatik

Informations

• Publié par: technische_universitat_munchen
• Publié le: 01 janvier 2007
• Nombre de lectures: 37
• Langue: English
• Poids de l'ouvrage: 2 Mo

Extrait

Model-based runtime analysis of
distributed reactive systems
Andreas Klaus BauerInstitut fur Informatik¨
der Technischen Universitat Munchen¨ ¨
Model-based runtime analysis of
distributed reactive systems
Andreas Klaus Bauer
Vollstandiger Abdruck der von der Fakultat fur Informatik der Tech-¨ ¨ ¨
nischen Universitat Munchen zur Erlangung des akademischen Grades¨ ¨
eines
Doktors der Naturwissenschaften (Dr. rer. nat.)
genehmigten Dissertation.
Vorsitzender: Univ.-Prof. Dr. Alois Knoll
Prufer der Dissertation:¨
1. Univ.-Prof. Dr. Dr. h.c. Manfred Broy
2. Dr. Perdita Stevens, Reader,
University of Edinburgh, UK
Die Dissertation wurde am 20.12.2006 bei der Technischen Univer-
sitat Munchen eingereicht und durch die Fakultat fur Informatik am¨ ¨ ¨ ¨
20.04.2007 angenommen.ivAbstract
As interactions and dependencies within distributed reactive systems increase, the
problem of detecting failures which depend on the exact situation and environmental
conditions they occur in grows. As a result, not only the detection of failures is
increasingly difficult, but also the differentiation between the symptoms of a fault,
and the actual fault itself, i.e., the cause of a failure.
This thesis proposes an efficient approach for the analysis of distributed reactive
systems at runtime. It introduces a framework, referred to as monitoring-based run-
time reflection framework, for the detection of failures as well as identification of
their causes. As an interface to the framework, this thesis proposes a specification
language, Salt, to express desired system properties, which then have to hold at
all times while a system executes. Detection of failures in the framework is based
upon monitoring systems with respect to their associated properties, defined in the
high-level specification language Salt. Salt specifications are translatable into the
real-time temporal logic TLTL as well as in the untimed temporal logic LTL, and
as such can also be used with other temporal logic verification frameworks, such as
model checkers. For both logics, an efficient monitor generation procedure is devel-
oped for either monitoring qualitative assertions about a system’s behaviour in the
untimed case, or quantitative assertions reflecting dense real-time constraints. In
order to reflect the semantics of LTL, respectively TLTL, with respect to a finite ob-
servational trace in a suitable and unambiguous manner, a 3-valued interpretation is
proposed. The corresponding 3-valued monitoring procedure is shown to be optimal
with respect to the space-complexity of the generated monitors, and able to detect
allminimalbadprefixesofnon-conformingsystembehaviour. Basedontheresultsof
the monitors, a dedicated failure diagnosis is performed to identify possible explana-
tions for an observed deviation. As such, diagnosis can either confirm that a monitor
detected the root cause for a failure, or indicate that the fault is located elsewhere,
and possibly outside the scope of the monitored system. In the runtime reflection
framework, diagnosis is based upon the principles of first-order model-based diagno-
sis, but developed in the propositional domain. The propositional diagnosis problem
is then shown to correspond to a deterministic implementation of a solution to the
#SAT problem for which a computationally efficient realisation is introduced.
This thesis develops both the theoretical foundations for runtime reflection as well as
efficient means for its implementation.
vviAcknowledgements
First and foremost, I want to express my gratitude to Manfred Broy for taking
me on in his highly energetic research group as well as for the supervision of this
thesis. Manfred Broy created a unique research and work environment for his group
from which I and my ideas have greatly benefited over the last almost four years.
Further, I want to thank Perdita Stevens from the University of Edinburgh for co-
supervising this thesis. Her acceptance of this task was beyond any call of duty, and
not always easy over a considerable spatial distance.
Martin Leucker must be pointed out as my academic role model over the past few
years. He had major influence on my development as an academic and researcher.
Selfishly, I made various people read through and comment on drafts of this thesis.
Timothy Bourke, Peter Braun, Gerwin Klein, Wendy Proctor, Michael Tautschnig,
and Martin Wildmoser even took the time to read and critically comment on almost
the entire document. I would like to sincerely thank them for their efforts.
Moreover, I am grateful for many stimulating and interesting discussions on topics
of this thesis (or, at first sight, rather unrelated themes, which later turned out
to be very influential) with Michael Beetz, Meir Manny Lehman, Reinhold Letz,
Hans-Wolfgang Loidl, Roland Martin, Christian Schallhart, Bernhard Sch¨atz, Anika
Schumann, and Gernot Stenz. Their broad experience and technical insights have
directly or indirectly shaped many different aspects of this thesis.
I also could not have done it without the moral support from various colleagues in
our group, and friends I have found within. In particular, I would like to point
out the members of the BASE.XT team as well as Johannes Gru¨nbauer who has
alwaysbeenapleasantofficemateandadearfriend. MarkusPizkadeservesaspecial
mention without whom I would probably not even have ended up in Manfred Broy’s
Software & Systems Engineering group at all. He also supported me with counsel
and encouragement when I needed it.
Finally, thanks are due to my colleagues and collaborators from industry with whom
I had the pleasure of working with foremost in the research projects AutoMoDe and
BASE.XT. In particular, I would like to thank Richard Bogenberger and Martin
Wechs from the BMW Group for many pleasant and interesting discussions which,
after all, centred not always around automotive software.
Andreas Bauer
Mu¨nchen, November 2006
viiviiiChronology
Muchof§3isbaseduponmaterialdevelopedbyBaueretal.[2006c],andsubsequently
published at the Eigth International Conference on Formal Engineering Methods
(ICFEM, see Bauer et al. [2006d]). The approach to runtime verification described in
§4isbaseduponresultsdevelopedfirstbyArafatetal.[2005], andsubsequentlypub-
lished at the 26th Conference on Foundations of Software Technology and Theoretical
Computer Science (FSTTCS, see Bauer et al. [2006b]). The approach to diagnosis as
developed in§5 has been published in large parts at the International Conference on
Integration of AI and OR Techniques in Constraint Programming for Combinatorial
Optimization Problems (CPAIOR, see Bauer [2005]). Various aspects of §6 (as well
as earlier chapters) are based upon a contribution to the IEEE Australian Software
Engineering Conference (ASWEC, see Bauer et al. [2006a]). Further implementa-
tion aspects detailed on in§6 are accepted for publication at the 2007 Conference on
Design, Automation and Test in Europe (DATE, see Bauer et al. [2007]).
Moreover, some minor results from papers for the USENIX Annual Technical Con-
ference (see Bauer [2004]), the 2005 ACM Conference on Embedded Software (EM-
SOFT, see Romberg and Bauer [2004]), and for the journal Informatik – Forschung
und Entwicklung (see Bauer et al. [2005]) are used and referred to throughout this
thesis.
ixx