A formal fault model for component based models of embedded systems [Elektronische Ressource] / von Marco Fischer
141 Pages
English

A formal fault model for component based models of embedded systems [Elektronische Ressource] / von Marco Fischer

Downloading requires you to have access to the YouScribe library
Learn all about the services we offer

Description

πderolicrwvodierteizurChecWissenschaftlichentSchriftenreiheertragen.Eingebonnenettete,herselbstozurganisierendeerdenSystemeLeserDervvierteaufBandherdernwissenscallenhaftlicDekhenhniscScBi-SimhriftenreihedenEingebtheoretiscettete,omplexenselbstorSoganisiertigken-ltendewirdSystemekwidmetwsicmicher?endertigenEnhentn,wireudecDr.klungf?rvhenzeonChemnitzFBez?geehlermosodeelMolenhergestellt.f?rErgebnisseeingebeinemettete,anscvierteilteannMulti-Prozessorsysteme.M?cDdesikenacseziehenwvierterdentzuMethoeinemeiterehierarczuhischhenHerrnNetzwdieerkhundwiczeiturwissenscSteue-hriftenreiherunghabvw?nsconvielFlugzeugenNutzen(ALekt?re.vionik)olframvFerbundenWissenscundUnivmehrtrumundemehrebruarimteAutomotivzureulationBereicwiehMeingesetzt.thoHierdesgiltdelleskingsh?DiechenhstewSicanherheitsstandardskeinzuhaltenBeispielundhau-maximalehVllustriert.erf?g-kbarkdereitdiezuhgaraneittiereenn.wicHerreFiscAnsatzesherhinoll-tegriertunddiemotiMo,dellierungenvwiconeltem?glicdikhenwFAnehlernendungsf?llein?bdeIcnfreueEnh,tFiscwurfsprozess.f?rAufVGrundlagetlicdesungVErgebnisseseiner-Kalk?lshenArbtiwicdieserkhaftliceltScHerrgewFisczuhereeinundforma-helesLesernFFehlermounddell,bdasdereineProf.einheitlicWheHardtMoandellierungakult?tvInformatikonhaftlicFLeiterehlerf?llenersit?tsrecunnterst?tzt.

Subjects

Informations

Published by
Published 01 January 2006
Reads 16
Language English
Document size 1 MB

π
orwolicder2007rtdiezurbWissenschaftlichenChecSchriftenreihetEingebertragen.ettete,gewselbstohaftlicrganisierendezuSystemeerdenDerLeserviertevBandaufderherwissenscihaftlichehenHardtSctechriftenreiheBi-SimEingebdenettete,theoretiscselbstoromplexenganisierSoen-tigkdeltenSystemewirdwidmetksicwhmicderer?enEnhthaftlicwiecFklungProf.vakult?tonersit?tsrecFInformatikehlermoBez?gedesolelenMof?rhergestellt.eingebErgebnisseettete,einemvanscerteilteiMulti-Prozessorsysteme.annDM?cideseksenacwziehenerdenviertzuteinemMethohierarceiterehisczuhenhNetzwHerrnerkdieundhzseinerurArbSteue-dieserrungScvzuonundFlugzeugenLesern(Aundvionik)dervWerbundenanundInformatikmehrLeiterundnmehrhimFAutomotivteezurBereiculationhwieeingesetzt.MHierthogiltdesesdellh?kingscDiehstehenSicwherheitsstandardsaneinzuhaltenkundBeispielmaximalehau-Vherf?g-llustriert.barkkeitderzudiegaranhtiereeitn.enHerrwicFisceherAnsatzesinhtegriertoll-dieundMomotidellierung,venonwicm?gliceltehendikFwehlernAninendungsf?llede?bnIcEnfreueth,wurfsprozess.FiscAuff?rGrundlageVdestlicVung-Kalk?lsErgebnisseenwicttigenwiceitkneltwissenscHerrhenFischriftenreiheheronneneinhabforma-n,lesw?nscFallenehlermovieldell,reudedasNutzeneineeieinheitlicLekt?re.heDr.MoolframdellierungDekvFonf?rFWissenscehlerf?llenherunUnivterst?tzt.henzeDabtrumeihniscweerdenChemnitzinebruarteressanvΠ
blefortheexample.itconnescienotherticersitseriestheEmapproacbineddedofSelf-OrganizedoSyassThetemsreaderThethe4thherveolumeWofofthe2007scienyticeseriestoEingebhecettete,depictedselbstorpganisiercomplexitendemotivSystemeed(Em-gladbortaneddedseries.Self-OrganizedllSystems)fromoutlinesoftheSciencedesigntofecfaultmomofaults.delsinfortoemSimbelleddeddsdis-deltributedaremresultsultiaproitcessorforsystems.understandTheseofmandultitoprovcedologyssorIsystemsMrwillhisbresearcescienconnectedItoouayhierarcbhicalProf.netHardtwacultorkputtoticconertrolChemnitzaiofrplanesF(astandardisedvionics)anddellingalsofbTherebe,usedterestingmorectionsandthmoreBi-inulationthewautomotivasemethoarea.ofHereMoitciskingessenestablished.tialtheoreticaltoaremeeontcomplexhighestSosafetisyossiblestandardstheandtototheensureythethismaximhumisofatedausevdeailabilitelopymetho.inMrapplications.FiscamherthatinFisctegratespublishestheimpmotdellinghofthispticotenSotialhopfaultsyinwitoenjothereadingdesignandprenetoit.cess.Dr.BasedolframonDeantheFPreamy-calculus,ComheerdevScienelopsHeadaUnivformalsiframewyork,UnivwhicyhTsupphnologyortsebruaryaviA Formal Fault Model for
Component-based Models of
Embedded Systems
Dissertation
Schriftliche Arbeit zur Erlangung des akademischen Grades
Doktoringenieur
(Dr.-Ing.)
an der Fakultat fur Informatik¨ ¨
der Technischen Universitat Chemnitz¨
von Dipl.-Inf. Marco Fischer
Gutachter: Prof. Dr. habil. Wolfram Hardt
Prof. Dr.-Ing. habil. Dieter Monjau
Prof. Dr. rer. nat. Franz Josef RammigAcknowledgements
As it would not have been possible to write this thesis without help, I would like to take
this chance to thank a few people.
First of all, I would like to thank Prof. Dr. Dieter Monjau, who generously supported
methroughoutandbeyondmystudiesattheChemnitzUniversityofTechnologyandwho
encouraged me to take the opportunity of writing this thesis. Without his initiative, I
probably would not have done it. I am also greatly indebted to Prof. Dr. Wolfram Hardt
for his outstanding support and for motivating me to complete the work.
Furthermore, I would like to thank my best friend Stefan, whom I have been knowing
for quite a long time now. Our many discussions about technical details were all
enlightening and surely influenced the ideas presented in this work in a positive way. Good luck
for your own thesis! I am equally grateful to Dr. Andr´e Windisch. Having such a good
guide and friend makes life a lot easier. Thank you for all the advice, for the time and
nerves spent reading the unfinished thesis several times and for always giving valuable
feedback.
Thanks go to all my former colleagues at EADS, especially to Maik Pitzen, Rainer
Werner, Lars Thalheim and Johann Schreyer. I like to remember the kind atmosphere at
work and the relaxing hours we spent doing barbecue at the river Isar. Special thanks
go to Chris Heald, Paul Warton and Lindsay Evans (all University of York) for the good
time we had when they did their internship at EADS and for proofreading publications
in English. I think that my writing skills have improved during that time.
This thesis resulted from work at EADS Military Aircraft in Ottobrunn. Therefore, I
thank Mr. Burkhard Balser for partially funding this work.
I am furthermore truly grateful to my parents, who never pushed me, but always
encouraged and supported me at best. Finally, and most of all, I thank my girlfriend
Sindy for her patience. It is probably not very easy to live with someone, who is often
distracted and who seems to be more interested in his work than in oneself.
Taufkirchen, 11. July 2006 Marco Fischer2Contents
1 Introduction 11
1.1 Faults, Errors, Failures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.2 Organisation of this Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2 Foundations 17
2.1 System Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.1.1 Basic System Concepts . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.1.2 Hierarchical System Descriptions . . . . . . . . . . . . . . . . . . . 18
2.1.3 System Specification Formalisms . . . . . . . . . . . . . . . . . . . 19
2.2 Process Calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.2.1 History. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.2.2 Basic π-calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.2.3 Typed π-Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
3 Related Work 31
3.1 Classification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3.2 Embedded Systems Modelling and Description Formalisms . . . . . . . . . 32
3.2.1 Embedded System Modelling . . . . . . . . . . . . . . . . . . . . . 32
3.2.2 Timed Description Formalisms . . . . . . . . . . . . . . . . . . . . . 32
3.3 Fault Modelling Approaches . . . . . . . . . . . . . . . . . . . . . . . . . . 33
3.3.1 Classification of Faults . . . . . . . . . . . . . . . . . . . . . . . . . 33
3.3.2 Fault Modelling at System Level . . . . . . . . . . . . . . . . . . . 35
3.3.3 Faults Modelled by Program Transformations . . . . . . . . . . . . 37
4 System Model 39
4.1 Hierarchical Structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
4.1.1 Logical Structuring of Models . . . . . . . . . . . . . . . . . . . . . 40
4.1.2 Components . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
4.1.3 Attributes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
4.1.4 Views . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
4.1.5 Ports and Methods . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
4.1.6 Layers, Platforms, Applications . . . . . . . . . . . . . . . . . . . . 464 CONTENTS
4.1.7 Binding applications to platforms . . . . . . . . . . . . . . . . . . . 48
4.2 Behaviour . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
4.2.1 Basic Values and Expressions . . . . . . . . . . . . . . . . . . . . . 53
4.2.2 Timed π-Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
4.3 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
5 Formal Fault Modelling 65
5.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
5.2 Fault Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
5.3 Fault Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
5.3.1 Local Fault Assumptions . . . . . . . . . . . . . . . . . . . . . . . . 71
5.3.2 Fail-stop . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72
5.3.3 Crash . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
5.3.4 Send Omission . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
5.3.5 Receive Omission . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
5.3.6 General Omission . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
5.3.7 Byzantine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
5.3.8 Partial Fault Models . . . . . . . . . . . . . . . . . . . . . . . . . . 78
5.3.9 Value Fault Models . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
5.3.10 Encoding of Components in Fault Calculus . . . . . . . . . . . . . . 80
5.3.11 Global Fault Assumptions . . . . . . . . . . . . . . . . . . . . . . . 82
5.4 Fault Tolerance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
5.4.1 Definition of Fault tolerance . . . . . . . . . . . . . . . . . . . . . . 82
5.4.2 Fault Tolerance based on strong bisimilarity . . . . . . . . . . . . . 83
5.4.3 Fault Tolerance based on weak bisimilarity . . . . . . . . . . . . . . 84
5.4.4 Generalisation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
5.4.5 Relation to Temporal Logic and Model Checking . . . . . . . . . . 87
5.4.6 Generalised Definition of Fault Tolerance . . . . . . . . . . . . . . . 90
5.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
6 Extended Example 93
6.1 Nominal Behaviour . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93
6.2 Faulty behaviour . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
6.3 Fault Tolerance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96
6.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102
7 Conclusion and Outlook 105
7.1 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
7.2 Limitations and Open Issues . . . . . . . . . . . . . . . . . . . . . . . . . . 106
7.3 Fault injection and simulation . . . . . . . . . . . . . . . . . . . . . . . . . 108CONTENTS 5
7.4 Fault Diagnosis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
7.5 Fault Tolerance Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
A Process Contexts 111
B An Intermediate Representation 113
Bibliography 121
Theses 1376 CONTENTSList of Figures
1.1 The fault-error-failure chain. . . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.2 Chapter dependencies. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.1 Basic system concepts. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.2 Hierarchical system seen as a white-box. . . . . . . . . . . . . . . . . . . . 18
2.3 The hierarchy of typed entities. . . . . . . . . . . . . . . . . . . . . . . . . 27
3.1 Communicating processes and an intercepting process modelling a fault. . . 36
4.1 The domain model packages. . . . . . . . . . . . . . . . . . . . . . . . . . . 40
4.2 The Package model object and related hierarchy. . . . . . . . . . . . . . . . 41
4.3 The Component model object. . . . . . . . . . . . . . . . . . . . . . . . . . 41
4.4 The PartsView model object and related hierarchy. . . . . . . . . . . . . . 43
4.5 The Port model object and related hierarchy. . . . . . . . . . . . . . . . . . 44
4.6 Provided and required method model objects hierarchy. . . . . . . . . . . . 45
4.7 Ambiguous forwarding of a provided method. . . . . . . . . . . . . . . . . 45
4.8 A Component with PartsView. . . . . . . . . . . . . . . . . . . . . . . . . 46
4.9 The Layer concept. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
4.10 The Instance model object and related hierarchy. . . . . . . . . . . . . . . 48
4.11 Binding an application on a platform. . . . . . . . . . . . . . . . . . . . . . 49
4.12 Layered behavioural description approach. . . . . . . . . . . . . . . . . . . 52
4.13 TLTS of a time guarded process. . . . . . . . . . . . . . . . . . . . . . . . 62
4.14 Illustration of ACTIVE according to equations a) 4.22 and b) 4.23. . . . . 64P0
5.1 A partition suffering a send omission fault. . . . . . . . . . . . . . . . . . . 74
5.2 Comparison of a) nominal and b) faulty behaviour with F . Note, thatRO
the numbers in parenthesis refer to the equations, where the corresponding
transition was derived. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
5.3 An example component C with two sub-components C1,C2 and the
corresponding structured calculus expression. . . . . . . . . . . . . . . . . . . 81
5.4 A scenario of fault tolerance. . . . . . . . . . . . . . . . . . . . . . . . . . . 83
5.5 Illustration of possibly-S.. . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
5.6 Illustration ofS-convergence. . . . . . . . . . . . . . . . . . . . . . . . . . 87