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

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.

Sujets

• Informatik

Informations

• Publié par: technische_universitat_chemnitz
• Publié le: 01 janvier 2006
• Nombre de lectures: 16
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

π
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 be