Formal Methods for Industrial Critical Systems: 14th International Workshop, FMICS 2009, Eindhoven, The Netherlands, November 2-3, 2009. Proceedings

front-matter......Page 1
Introduction......Page 10
Bi-Abduction......Page 11
Compositional Shape Analysis......Page 12
Application to Real Code......Page 13
References......Page 17
Introduction......Page 18
Preliminaries......Page 20
A Language for CTMCs......Page 23
Fully Markovian Stochastic Process Calculi......Page 24
$TIPP_k$......Page 25
$PEPA_k$......Page 26
A Language of Interactive Markov Chains......Page 28
Conclusions......Page 31
References......Page 32
Proof of Proposition 1......Page 33
Introduction......Page 35
The Genesis......Page 36
Embedded Software......Page 37
Platform Screen Doors......Page 38
SmartCard......Page 40
Animation and Documentation......Page 41
Conclusion......Page 42
References......Page 43
What’s in Common between Test, Model Checking, and Decision Procedures?......Page 44
References......Page 45
Introduction......Page 46
The RC4 Cipher and Its Implementation in openSSL......Page 48
Functional Correctness of Code Refactoring......Page 50
Proving Equivalence Using Natural Invariants......Page 54
Implementation Details......Page 57
Conclusions......Page 58
References......Page 59
openSSL Implementation of RC4......Page 61
Introduction......Page 62
Accuracy and Sensitivity Analyses......Page 63
The IEEE-754 Standard......Page 64
General Description......Page 65
Specific Abstract Domains Based on Affine Arithmetic......Page 66
Use and Main Features of FLUCTUAT......Page 67
Families of Basic Operators......Page 68
The Analysis Process......Page 69
Analyzing Interpolation Operators......Page 70
Analyzing Recursive Operators......Page 74
Conclusions and Future Work......Page 76
References......Page 77
Introduction......Page 79
Partitioning the State Space......Page 81
Related Work......Page 82
Dynamic Partitioning Based on Refinement......Page 84
Selection of Candidate Components......Page 87
Experiments......Page 89
Conclusions and Future Work......Page 93
References......Page 94
Introduction......Page 95
Protocol Requirements......Page 96
Protocol Stack......Page 97
Ether......Page 98
Link Layer......Page 99
Guaranteed Delivery Protocol......Page 100
Application Layer......Page 101
Protocol Verification......Page 102
Proving Invariants on WDP and GDP, Independently......Page 104
Proving Invariants on the Asynchronous Composition of WDP and GDP......Page 106
Related Work and Conclusion......Page 108
References......Page 109
Introduction......Page 111
The Recycling Plant Example......Page 113
Design of a Resource-Based Solution......Page 114
Anatomy of a Specification......Page 115
Translating Shared Resources into TLA......Page 117
Anatomy of a Translation......Page 118
Verifying System Properties Using TLC......Page 119
Cooking the Processes......Page 120
Checking System Properties......Page 122
Conclusion......Page 123
References......Page 125
Introduction......Page 126
Current Platforms for Java Programs......Page 128
Java Platforms for Embedded Systems......Page 129
Running Example......Page 130
Java PathFinder......Page 132
Restrictions of Concurrency in Model Checking Java Programs with Java PathFinder......Page 133
Experiments......Page 135
Evaluation and Related Work......Page 137
Conclusion......Page 139
References......Page 140
Introduction......Page 142
Basic Concepts......Page 144
Semantics of UDPs......Page 145
Commuting Diamond Analysis......Page 147
Verilog Timing Checks......Page 151
Required Permutations for Reachability Analysis......Page 153
Non-deterministic Reachability Analysis......Page 154
Experimental Results......Page 156
References......Page 157
Composing Services......Page 158
Service Composition Methodology......Page 159
Relationship to Other Work......Page 160
Service Composition and Grid Services......Page 161
Cress......Page 162
Describing Service Composition......Page 163
Formalising Service Composition......Page 166
Annotating Lotos......Page 168
Verifying Service Compositions......Page 169
Implementing and Deploying Composed Grid Services......Page 171
Conclusion......Page 172
References......Page 173
Introduction......Page 174
The Safe Language......Page 176
The Safe Virtual Machine......Page 177
Formalisation of the JVM in Isabelle/HOL......Page 180
Mapping the SVM Data Structures......Page 182
Mapping the SVM Code......Page 183
Translation Functions......Page 184
Certification of the Implementation......Page 185
Conclusions and Related Work......Page 187
References......Page 188
Formal Development for Railway Signaling Using Commercial Tools......Page 190
References......Page 191
Problem Statement......Page 192
Qualification of Critical Code Generators......Page 193
References......Page 194
Motivation......Page 195
Conclusion......Page 196
References......Page 197
Behavioural Analysis of an I$^{2}$C Linux Driver......Page 198
References......Page 199
Model-Based Testing of Electronic Passports......Page 200
References......Page 201
Modeling Hybrid Systems with PROMELA......Page 203
DSTwithSPIN......Page 204
References......Page 205
back-matter......Page 206