A formal framework for modelling component extension and layers in distributed embedded systems [Elektronische Ressource] / von Stefan Förster
228 Pages
English

A formal framework for modelling component extension and layers in distributed embedded systems [Elektronische Ressource] / von Stefan Förster

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

Description

ππonsistenzrwakult?toausf?hrlicrtationen.zurormWissenschaftlichenhaftlicSchriftenreiheUnEingeboettete,ErselbstoundrganisierendeF?rsterSystemeFDerUnivvliegtorliegendeompBandezikder?fwissenscEihaftlicKhenksvScArbhriftenreihedieserEingebzuettete,Prof.selbstorersit?tsrecgani-wsiervendevSystemem?glicwidmetzusicundhKdemsiertEnbtundwurfinvannonnacvtigkerteiltenBewEingebdieettetenfreueSystemen.er?enEinsatzgebieteeitsoftelcheherbSystemeHardtsindhaftlicunTterebruaranderemunktMissions-hundHerrnSteuerungssystemeErwvSystemsponwirdFlugzeugenT(AnerospaceeAnzuwGesamendungen)onund,undmitt?bzunehmendern.Vklarernetzung,ei-dernacAu-btomotiv-Kalk?leusBereicF?rsterh.seinesHierwgiltM?cesein-h?uncstellen.hsteBeispielSicanzherheitsstandardsIceinzuhaltenh,unddiemaximalehVherf?gbarkdiesereitSczugewgaranen,tieren.LesernHerrundF?rsterdernimmWtansicInformatikhLeiterdiesernProblematikhniscinChemnitzeinemvsehrerpfr?henderStadiumtersucdesungenEnontF?rsterwurfsprozesses,aufdereiterungenSponezikezikationsphase,Soan.esEsh,weilkerdenoneImple-tenmenvtierungsvr?ndernariandertensubstituierenwiedieHardwtspareatiundaufSoftorrektheitwKareautomasoiwiezuSystemkerprompeonen?tenerwiedenierteBere-wcterungsrelationenhformalungskhpr?fbareompnonenettungtendenoundFKalismommkunikHerrationskdieomporrektheitonenAnsatzestenhuneisenterscdiehieden.hF?reitdiedruc?bollergrei-terfendeeisSpEinezikhesationzeigtenPraxisrelevtdieserwiceit.kheltmicHerrHerrnF?rsterf?

Subjects

Informations

Published by
Published 01 January 2006
Reads 13
Language English
Document size 2 MB

π
π
onsistenzrwakult?toausf?hrlicrtationen.zurormWissenschaftlichenhaftlicSchriftenreiheUnEingeboettete,ErselbstoundrganisierendeF?rsterSystemeFDerUnivvliegtorliegendeompBandezikder?fwissenscEihaftlicKhenksvScArbhriftenreihedieserEingebzuettete,Prof.selbstorersit?tsrecgani-wsiervendevSystemem?glicwidmetzusicundhKdemsiertEnbtundwurfinvannonnacvtigkerteiltenBewEingebdieettetenfreueSystemen.er?enEinsatzgebieteeitsoftelcheherbSystemeHardtsindhaftlicunTterebruaranderemunktMissions-hundHerrnSteuerungssystemeErwvSystemsponwirdFlugzeugenT(AnerospaceeAnzuwGesamendungen)onund,undmitt?bzunehmendern.Vklarernetzung,ei-dernacAu-btomotiv-Kalk?leusBereicF?rsterh.seinesHierwgiltM?cesein-h?uncstellen.hsteBeispielSicanzherheitsstandardsIceinzuhaltenh,unddiemaximalehVherf?gbarkdiesereitSczugewgaranen,tieren.LesernHerrundF?rsterdernimmWtansicInformatikhLeiterdiesernProblematikhniscinChemnitzeinemvsehrerpfr?henderStadiumtersucdesungenEnontF?rsterwurfsprozesses,aufdereiterungenSponezikezikationsphase,Soan.esEsh,weilkerdenoneImple-tenmenvtierungsvr?ndernariandertensubstituierenwiedieHardwtspareatiundaufSoftorrektheitwKareautomasoiwiezuSystemkerprompeonen?tenerwiedenierteBere-wcterungsrelationenhformalungskhpr?fbareompnonenettungtendenoundFKalismommkunikHerrationskdieomporrektheitonenAnsatzestenhuneisenterscdiehieden.hF?reitdiedruc?bollergrei-terfendeeisSpEinezikhesationzeigtenPraxisrelevtdieserwiceit.kheltmicHerrHerrnF?rsterf?raVuftlicGrundlageungdeswicVtigenArb-Kalk?lsineinwissenscformaleshenFhriramewnreiheork,onnendashabeinew?nsceinheitlicallenhevielMoreudedellierungNutzenveionLekt?re.TDr.eilsystemenolframinDekdenFunf?rterscWissenschied-herlicUnivhenhenzeEntrumtecwurfsphasenheunersit?tterst?tzt.FBesonderer2007SchΠ
Π
nforsetheenetscieneticIseriesofEmofbkeddedybleSelf-organizedscienSystemsticThisortsvdierenolumeofoforthethescienapproacticformallyseriestheEingebhisettete,ouselbstordeanganisierpuende-calculus,Systemend(EmofbTheed-hdedThereforeSelf-moOandrganiandzMredtheSystems)impressivgivdenedesbandetailedoofutthatlresearcineIofreadingtheDr.designofofersitdistributedChemnitzemFbheddedstsystems.rFieldsmoofdulesapplicationdesignforfosucF?rster'shthesystemsspare,willamongstossibleothers,imissionmosystemscandtheconstencytrolspsystemscofvairplanesof(aeronauticandapplithecyarelationsteriableiinons)formalism.andsho-relevwithresearcincreasinggllevF?rsterelortanofininseries.tegratione-enjoalsoandtheit.automotivolframefacultarea.scienceInofthiscarecenaersitiect2007iwhicssuppessenatialatoameetdihighestdsafetdellingymostandardsinandttosteps.ensuremainthecusmaximMruresearcmisofextensionasystemvecications.ailabilitityb.pMrtoF?rsterdaddressesfythesesubstituteproblemsdulesintoanhecearlyautomaticallystatecorrectnessofconsi-theofdesigntotalproecication.cess,F?rsternamelyatheprospeecication.correctnessImplemenhista-htiondemonstratesvelyersionscomplexitlikbeclearlyhardwextensionareandandvsoftemweddingaretheare-calculusdierenAtiatedexampleaswswpracticalellanceasthissystemh.camoadmpMronenpublishestsimpliktehcomputationthiscompticonenSotshopandycommwillunicatioynitcompbonenfromts.Prof.FWorHardtaofgeneralyspcomputerecica-scientiondirectorMrunivF?rsterydevomelopsteratreformalUnivframewyorkTbasedhnologyonebruarytheviPreamA Formal Framework for Modelling
Component Extension and Layers in
Distributed Embedded Systems
Dissertation
Schriftliche Arbeit zur Erlangung des akademischen Grades
Doktoringenieur
(Dr.-Ing.)
an der Fakult¨at fur¨ Informatik
der Technischen Universitat¨ Chemnitz
von Dipl.-Inf. Stefan F¨orster
Gutachter: Prof. Dr. habil. Wolfram Hardt
Prof. Dr.-Ing. habil. Dieter Monjau
Prof. Dr. rer. nat. Franz Josef RammigAcknowledgements
This work would not exist without the support, encouragement, and help of many people.
First of all, I am indebted to Prof. Dr.-Ing. habil. Dieter Monjau who encouraged me to
persuade a PhD degree in the first place. I am grateful because even after his emeritus
he continued in supporting this work. Moreover, during the countless fruitful discussions
many ideas for this work took shape.
IalsothankProf. Dr. habil. WolframHardtforsupportingthisthesis. Inanindustrial
environment he helped me to keep in touch with the scientific world.
Furthermore, Iam indebtedtoProf. Dr. rer. nat. FranzJosefRammigforhis interest
in this thesis and for being on the PhD committee.
I am grateful to some personal friends which I had the privilege to work with in
the AGS (Automatische Generierung von Systemtabellen) team. With joy I remember the
threeyearsweworkedtogetherontheimplementationoftheVERDI(Verified Engineering
of Runtime Blueprint Data for IMA Systems) toolset, the discussions in the beer gardens,
andthecollaborativepaperwriting. Inparticular,IthankDr. Andr´eWindischandMarco
Fischer for their friendship and for reading and commenting this thesis. Without their
help,manyofthepresentedideaswouldbeexpressedlessclearly. Iamalsoindebtedtoour
internswhoworkedoverthetimeintheAGSteam. AmongthemareChrisHeald,Lindsay
Evans, Paul Barton, Juliane Knopp, and Eugen Riegel, who helped in implementing the
VERDI toolset and proof-read many of our joint papers.
Also, I would like to thank my former colleagues of the New Avionics Structures
department at the EADS (European Aeronautic Defence and Space Company). Their
expert knowledge in the domain of avionics systems broadened my mind, helped me to
keep an eye on real world problems, and gave this thesis a practical relevance. Especially,
I am grateful to Andreas Nuscheler and Burkhard Balser for giving me the opportunity
to work as a PhD student for the EADS and for funding this work.
Further, I thank my new colleagues in the EPAS (Engineering Platform for Au-
tonomous Systems) team for their support and encouragement. In particular, I thank
Dr. Norbert Oswald for offering me a position in the EPAS team. I am also indebted to
Toni Reichelt and Herwig Moser for proof-reading, commenting, and discussing the final
version of this work.
Last but not least, I thank my family. I am grateful to my parents for continuously
supportingmyeducation. Finally,IthankmywifeSilkeandmysonErik. Theirlove,care,2 ACKNOWLEDGEMENTS
support, and encouragement helped me more than words can express. Without them, I
would have never been able to continue and finish this work.
Stefan F¨orster
Munich, October, 2006Contents
Acknowledgements 1
Contents 3
List of Tables 7
List of Figures 9
List of Acronyms 11
List of Symbols 17
Abstract 19
1 Introduction 21
1.1 The Domain of Distributed Embedded System Design . . . . . . . . . . . . 22
1.2 Scope of the Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
1.3 Outline of the Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2 Related Work 27
2.1 The Semantics of Components and Systems . . . . . . . . . . . . . . . . . . 27
2.1.1 State Based Formalisms . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.1.2 Process Algebraic Formalisms . . . . . . . . . . . . . . . . . . . . . . 28
2.1.3 Combined Formalisms . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.1.4 Other formalisms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.2 Subtyping and Inheritance . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.2.1 Subtyping in Process Algebras . . . . . . . . . . . . . . . . . . . . . 30
2.2.2 Subtyping in other Formalisms . . . . . . . . . . . . . . . . . . . . . 32
2.3 System Modelling Languages and Approaches . . . . . . . . . . . . . . . . . 33
2.3.1 Architecture Description Languages . . . . . . . . . . . . . . . . . . 34
2.3.2 UML based Modelling Languages . . . . . . . . . . . . . . . . . . . . 39
2.3.3 Other Modelling Approaches . . . . . . . . . . . . . . . . . . . . . . 424 CONTENTS
3 Foundations 45
3.1 Simply-Typed Pi-Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
3.1.1 Syntax of Processes . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.1.2 Type System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
3.1.3 Typed Abstractions . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
3.1.4 Semantics of Processes . . . . . . . . . . . . . . . . . . . . . . . . . . 50
3.1.5 Process Congruence . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
3.1.6 Equivalence Relations . . . . . . . . . . . . . . . . . . . . . . . . . . 53
3.2 Pi-Calculus with Structured Types and Subtyping . . . . . . . . . . . . . . 57
3.2.1 Syntactic Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
3.2.2 Type System Extensions . . . . . . . . . . . . . . . . . . . . . . . . . 58
3.2.3 Additional Transition Rules . . . . . . . . . . . . . . . . . . . . . . . 61
BV ,#,⊕,×,μ,i/o3.2.4 Process Congruence in π . . . . . . . . . . . . . . . . . 63
4 Extension Relations 65
4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
4.1.1 Substitutability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
4.1.2 Terminology and Notation . . . . . . . . . . . . . . . . . . . . . . . . 69
4.2 Process Extension Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
4.2.1 Interface Extension Relation . . . . . . . . . . . . . . . . . . . . . . 71
4.2.2 Cut-Off Extension Relation . . . . . . . . . . . . . . . . . . . . . . . 73
4.2.3 Closed Extension Relation . . . . . . . . . . . . . . . . . . . . . . . . 76
4.2.4 Open Extension Relation . . . . . . . . . . . . . . . . . . . . . . . . 82
4.3 A Constructional Approach to CCEP . . . . . . . . . . . . . . . . . . . . . 83
4.3.1 The Process Interaction Model . . . . . . . . . . . . . . . . . . . . . 83
4.3.2 The Value Buffer Model . . . . . . . . . . . . . . . . . . . . . . . . . 85
4.3.3 The Link Buffer Model . . . . . . . . . . . . . . . . . . . . . . . . . 88
4.3.4 The Closed Environment Model. . . . . . . . . . . . . . . . . . . . . 91
5 System Modelling Framework 97
5.1 The Component Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
5.1.1 Categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
5.1.2 Attributes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
5.1.3 Interface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
5.1.4 Views . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111
5.2 The Parts-View . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113
5.2.1 Physical Parts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115
5.2.2 Logical Parts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116
5.2.3 Connections . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117
5.3 The Integration-View. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120
5.3.1 Platform Components . . . . . . . . . . . . . . . . . . . . . . . . . . 121CONTENTS 5
5.3.2 Application Components. . . . . . . . . . . . . . . . . . . . . . . . . 121
5.3.3 Bindings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122
5.4 View Encodings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123
5.4.1 Parts-View Encoding . . . . . . . . . . . . . . . . . . . . . . . . . . . 123
5.4.2 Integration-View Encoding . . . . . . . . . . . . . . . . . . . . . . . 125
5.5 The Component Extension Relation . . . . . . . . . . . . . . . . . . . . . . 125
5.5.1 Handling of Simultaneous Extension . . . . . . . . . . . . . . . . . . 128
5.5.2 Behavioural Verification of Component Extension . . . . . . . . . . . 130
5.5.3 Non-Behavioural Verification of Component Extension . . . . . . . . 137
5.5.4 Extension Relation Consistency . . . . . . . . . . . . . . . . . . . . . 138
5.6 Modelling Layers and Layer Refinement . . . . . . . . . . . . . . . . . . . . 139
5.6.1 Layer Modelling . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 140
5.6.2 Layer Refinement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 144
6 Applications 147
6.1 Component Extension Example . . . . . . . . . . . . . . . . . . . . . . . . . 147
6.1.1 The Component Models . . . . . . . . . . . . . . . . . . . . . . . . . 148
6.1.2 Component Extension Verification . . . . . . . . . . . . . . . . . . . 154
6.2 Modelling Layered Applications . . . . . . . . . . . . . . . . . . . . . . . . . 157
6.2.1 The ASAAC Standard . . . . . . . . . . . . . . . . . . . . . . . . . . 157
6.2.2 Avionics System Modelling . . . . . . . . . . . . . . . . . . . . . . . 161
6.2.3 System Configuration . . . . . . . . . . . . . . . . . . . . . . . . . . 163
7 Conclusion 165
7.1 Results. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165
7.2 Open Issues . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167
7.3 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 168
A Reference to Extended Pi-Calculus 169
B Implementation 175
B.1 Component Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . 176
B.1.1 Attribute Implementation . . . . . . . . . . . . . . . . . . . . . . . . 176
B.1.2 Component Relations Implementation . . . . . . . . . . . . . . . . . 177
B.2 View Implementations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 178
B.2.1 Parts-View Implementation . . . . . . . . . . . . . . . . . . . . . . . 179
B.2.2 Integration View Implementation . . . . . . . . . . . . . . . . . . . . 181
B.2.3 Base-View Implementation . . . . . . . . . . . . . . . . . . . . . . . 182
B.3 Data-Type Implementations . . . . . . . . . . . . . . . . . . . . . . . . . . . 182
B.4 Layer Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 184
B.5 Packages & Projects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1846 CONTENTS
C Encodings and Verification Results 187
C.1 The Mobility Workbench (MWB) . . . . . . . . . . . . . . . . . . . . . . . . 187
C.2 Chapter 2 Encodings and Examples . . . . . . . . . . . . . . . . . . . . . . 188
C.3 Chapter 4 Encodings and E . . . . . . . . . . . . . . . . . . . . . . 189
C.3.1 Name Aliasing and Cut-Off Extension Example . . . . . . . . . . . . 189
C.3.2 Example of Cut-Off Extension . . . . . . . . . . . . . . . . . . . . . 189
C.3.3 Example of Closed Extension . . . . . . . . . . . . . . . . . . . . . . 189
C.3.4 Counter-Example for Non-Transitivity of Closed Extension . . . . . 190
C.3.5 Weak Bisimilarity of PIM IN and PIM IN NEW . . . . . . . . . . . 190
C.4 Chapter 6 Encodings and Examples . . . . . . . . . . . . . . . . . . . . . . 191
C.4.1 Component Extension Example – Encodings . . . . . . . . . . . . . 191
C.4.2 Component Extensione – Verification . . . . . . . . . . . . . 194
Bibliography 199
Index 215
Theses 221