Model-based development of fault-tolerant real-time systems [Elektronische Ressource] / Christian Buckl

Christian Buckl

Sujets

• Informatik

Informations

• Publié par: technische_universitat_munchen
• Publié le: 01 janvier 2008
• Nombre de lectures: 19
• Langue: Deutsch
• Poids de l'ouvrage: 1 Mo

Extrait

TECHNISCHEUNIVERSITÄTMÜNCHEN
LehrstuhlfürEchtzeitsystemeundRobotik
Model BasedDevelopmentofFault Tolerant
Real TimeSystems
ChristianBuckl
VollständigerAbdruckdervonderFakultätfürInformatikderTechnischenUniversität
MünchenzurErlangungdesakademischenGradeseines
DoktorsderNaturwissenschaften(Dr.rer.nat.)
genehmigtenDissertation.
Vorsitzender: Univ. Prof. Dr. Dr. h.c. ManfredBroy
PrüferderDissertation:
1. Univ. Prof. Dr. AloisKnoll
2. Prof. EdwardA.Lee
UniversityofCalifornia,Berkeley/USA
DieDissertationwurdeam05.05.2008beiderTechnischenUniversitätMünchen
eingereichtunddurchdieFakultätfürInformatikam22.09.2008angenommen.IIZusammenfassung
Die Entwicklung fehlertoleranter Echtzeitsysteme ist sehr komplex. Die Sys
teme müssen nicht nur Echtzeitbedingungen einhalten, sondern ihre Funktion
alitätauchunterdemEinflussvondurchdieHardwareund/oderdieSoftware
bedingten Fehlern erbringen. Um in einem System Fehlertoleranz zu erlangen,
mussRedundanzeingesetztwerden. DiesewirdhäufigdurchVerwendungvon
mehrerenRechnernineinemverteiltenSystemerzielt.
UmdiewachsendeKomplexitätderSoftwarezubeherrschen,werdeninderIn
formatik modellbasierte Entwicklungswerkzeuge eingesetzt. Die existierenden
Werkzeuge beschränken sich dabei jedoch zumeist auf die Modellierung und
Generierung der Anwendungsfunktionalität. Code für nicht funktionale As
pekte wie Fehlertoleranzmechanismen, Kommunikation oder Scheduling wird
nicht generiert. Diese Aspekte sind jedoch für einen Großteil der Komplexität
verantwortlich.
DieseArbeitstelltdahereinEntwicklungswerkzeugfürfehlertoleranteEchtzeit
systeme vor, welches die Generierung von Code zur Umsetzung dieser nicht
funktionalen Aspekte unterstützt. Dadurch werden existierende Entwick
lungswerkzeuge ideal ergänzt. Der Beitrag dieser Arbeit liegt insbesondere
in der Ausarbeitung von geeigneten Modellen zur Beschreibung und Code
generierung fehlertoleranter Systeme. Unter anderem erlauben die vorgestell
ten Modelle die formale Spezifikation der Hardwarearchitektur, eine präzise
Definition der Softwarekomponenten und ihres zeitlichen Verhaltens, die ein
deutigeFestlegungvonFehlerannahmen,sowiedieAuswahlgeeigneterFehler-
toleranzmechanismen.
Unter Verwendung eines vorlagenbasierten Codegenerators wird der
entsprechendeCodeerzeugt. DieErweiterungsmöglichkeitendesCodegenera
tors bieten eine Lösung für die vorherrschende Heterogenität der verwendeten
Ausführungsplattformen. Die Arbeit stellt eine generische Softwarearchitektur
vor und diskutiert die Umsetzung bekannter Fehlertoleranzmechanismen.
Zudem wird aufgezeigt, wie formale Methoden zur Verifikation integriert
werdenkönnen.
Anhand von zwei aussagekräftigen Anwendungen werden schließlich die
Vorteile des Ansatzes hervorgehoben. Die erste Anwendung zeigt, dass auch
SystememitRegelungszeitenimBereichvonwenigenMillisekundenbasierend
auf Standardhardware unterstützt werden. Die zweite Anwendung demon
striert, wie durch eine Kombination mit existierenden Werkzeugen eines der
wesentlichen Ziele im Bereich Software Engineering erreicht werden kann: die
hundertprozentigmodellbasierteEntwicklung-hierimKontextvonverteilten,
fehlertolerantenSystemen.
IIIIVAbstract
The design of fault tolerant real time systems is a complex task. The system
must not only satisfy real time requirements, but it must also deliver the spec
ified functionality in the presence of both hardware and software faults. To
achieve fault tolerance, the system has to use redundancy. This redundancy
isusuallyachievedbyreplicatinghardwareunitsandexecutingtheapplication
withinadistributedsystem.
Model based design tools promise to reduce the complexity of the design
process by raising the abstraction level. However, most of the existing tools fo
cusonlyonfunctionalaspects. Coderealizingnon functionalrequirementssuch
as fault tolerance mechanisms, communication, and schedulingis not targeted.
However,thistypeofcodemakesupthemajorityofthecodeofafault tolerant
real timesystem.
This work presents a model based development tool for the design of fault
tolerant real time systems. The tool focuses on the code generation of non
functional requirements and therefore complements existing tools. The major
contribution of this thesis is the presentation of adequate models that can be
usedtomodelfault tolerantsystemsandgeneratethecodeautomatically. These
models comprise a formal description of the hardware architecture, the soft
ware components and their temporal behavior, the fault assumptions, and the
selectedfault tolerancemechanisms.
Using a template based code generator, the fault tolerant real time system is
generated. The template based code generator allows an easy expansion of
the code generation functionality and therefore offers a solution to handle the
heterogeneity of fault tolerant systems. The thesis presents a generic architec
tureforfault tolerantsystemsanddiscussestherealizationofwell knownfault
tolerance mechanisms in this context. Finally, the thesis outlines how formal
methodscanbeintegratedtoprovethecorrectnessofthegeneratedcode.
Two complementary applications are used to demonstrate the practicability of
theapproach. Oneapplicationpointsoutthatcontroltimesintherangeofafew
milliseconds can be achieved using standard hardware. The second applica
tiondemonstratesthatbycombiningdifferenttools,onemajorgoalinsoftware
engineering can be achieved: the development of a complex and distributed
embeddedsysteminacompletemodel basedway.
VVIAcknowledgements
First of all, I want to thank my supervisor, Professor Alois Knoll, for provid
ingmetheopportunitytopreparethisthesisandforsupportingmyworkwith
ideas, criticism, motivation, and guidance. I am very thankful to Professor Ed
wardLeeforacceptingtobemyexternalreviewer.
ManythanksgototheentiregroupEmbeddedSystemsandRoboticsattheTU
Münchenforthevaluablediscussionsandthepleasantatmosphere. Inparticu
lar, I want to thank Simon Barner and Michael Geisinger for proof reading the
thesis, as well as Markus Rickert for answering all my questions regarding the
layout.
I also thank my family for accepting my role as a lost son in the last months.
Thanks to my parents Erika und Manfred for the wonderful education and all
the opportunities they offered me. Many thanks go to my sister Sabine who
helpedmeproof readingthisthesis.
Finally, very special thanks go to my girlfriend Katharina for supporting me,
especially during the last months. She gave me the extra strength, motivation,
andlovenecessarytogetthisthesisdone.
VIIVIIIContents
1 Introduction 1
1.1 BackgroundandMotivation . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 GoalsofthisThesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.3 MainContributionsofthisThesis . . . . . . . . . . . . . . . . . . . . . . . 5
1.4 StructureofthisThesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2 Background: Fault TolerantComputing 9
2.1 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.2 FormalSpecificationoftheSystem . . . . . . . . . . . . . . . . . . . . . . 15
3 OverviewoftheApproach 19
3.1 RequirementsontheTool . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
3.2 Template BasedCodeGenerationandDevelopmentSteps . . . . . . . . 22
3.3 CodeGenerationProcess . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
3.4 Demonstrators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
4 AdequateMeta Models 31
4.1 RequirementsontheMeta Model . . . . . . . . . . . . . . . . . . . . . . . 31
4.2 Overview: UsedMeta Models . . . . . . . . . . . . . . . . . . . . . . . . . 33
4.3 HardwareModel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
4.4 Software . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
4.5 FaultModel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
4.6 Fault ToleranceModel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
4.7 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
5 Realization 89
5.1 Run TimeSystemArchitecture . . . . . . . . . . . . . . . . . . . . . . . . 89
5.2 CommunicationComponent. . . . . . . . . . . . . . . . . . . . . . . . . . 91
5.3 Fault Tolerance . . . . . . . . . . . . . . . . . . . . . . . . . . 92
5.4olerantScheduling . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
IXContents
5.5 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112
6 Verification 115
6.1 ConceptforFormalVerification . . . . . . . . . . . . . . . . . . . . . . . . 116
6.2 FormalSpecificationoftheSystem . . . . . . . . . . . . . . . . . . . . . . 117
6.3 Prototype . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120
7 Conclusion 123
A RelatedWork-ModelingTools,CodeGeneratorsandFrameworks 125
A.1 UnifiedLanguage . . . . . . . . . . . . . . . . . . . . . . . . . . 125
A.2 Domain SpecificTools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126
A.3 Meta ModelingFrameworks . . . . . . . . . . . . . . . . . . . . . . . . . 127
A.4 CodeGenerators . . .