Formal Methods for Industrial Critical Systems: 13th International Workshop, FMICS 2008, L’Aquila, Italy, September 15-16, 2008, Revised Selected Papers

front-matter......Page 1
Formal Methods for Critical Systems......Page 10
Model-Based Verification of Automotive Control Software......Page 11
Contract-Based Analysis of Automotive and Avionics Applications: The SPEEDS Approach......Page 12
Panel Discussion on Formal Methods in Commercial Software Development Tools......Page 13
Introduction......Page 16
Development Process and Target Test Phase......Page 17
Requirements for an Automated Test Oracle Procedure......Page 18
Test Schemas......Page 20
Language for the Test Section......Page 21
Illustration......Page 23
Implementation of the Approach......Page 26
Experiments and Results......Page 29
Conclusion......Page 30
References......Page 31
Introduction......Page 32
Overview of Lustre......Page 34
Operator Network......Page 35
Clocks in Lustre......Page 36
Activation Conditions......Page 37
Coverage Criteria......Page 39
Activation Conditions for when and current......Page 40
An Illustrative Example......Page 42
Conclusion......Page 44
Introduction......Page 46
Overview of Techniques for Fighting State Space Explosion......Page 47
State Space Reductions......Page 48
Parallel and Distributed Computation......Page 49
Research Papers......Page 50
Quality of Experiments......Page 51
Reported Improvement......Page 52
On-the-fly State Space Reductions......Page 54
Distributed Exploration......Page 55
Conclusions......Page 56
Introduction......Page 62
Probabilistic Model Checking......Page 64
Algorithm......Page 67
Minimal Subgraph Identification......Page 68
Iterative Computation......Page 69
Trivial SCC......Page 71
Parallelization......Page 72
Experimental Evaluation......Page 73
Conclusion......Page 76
Introduction......Page 78
Transitions Systems......Page 79
Partial-Order Reduction......Page 80
The Two-Phase Algorithm......Page 81
Forward Symbolic Model-Checking of CTL......Page 82
Forward Model Checking with Partial Order Reduction......Page 84
Implementation......Page 87
Case Study......Page 89
Conclusion and Perspectives......Page 91
Introduction......Page 94
The Readers-Writers Problem......Page 95
Implementation of Read-Write Locks......Page 96
Model Checking Readers/Writers with Uppaal......Page 98
Correcting the Implementation/Model......Page 101
Readers-Writers Model in PVS......Page 102
Translation from Uppaal to PVS......Page 104
System Invariants......Page 105
No Deadlock......Page 106
Related and Future Work......Page 107
Concluding Remarks......Page 109
Introduction......Page 112
B Machines......Page 114
CSP||B Components......Page 115
The Driving System......Page 118
Specifying a Platoon of Cristals......Page 120
Three New CSP controllers......Page 122
The Vehicle2 Assembly......Page 123
Related Works......Page 125
Conclusion......Page 126
Introduction......Page 128
Related Work......Page 130
Functional and Performance Timing Requirements......Page 131
Requirements Refinement and SDV Procedure Overview......Page 132
Sample Instances......Page 133
Environmental Assumptions......Page 134
Latest Environment Based Feasibility Analyses......Page 135
Comparing the Feasibility Results in Different Environments......Page 137
Timer Implementation of Held_For_S......Page 139
Example: Delayed Trip System with Tolerances......Page 140
Summary......Page 142
Introduction......Page 144
Dynamic Automata with Events and Timers......Page 145
Constructing Monitors from DATEs......Page 149
Case Study......Page 151
Related Tools......Page 153
The Benchmark......Page 154
Performance of Larva......Page 155
Conclusions......Page 157
Introduction......Page 159
I/O Efficient Model Checking with Mechanical Disks......Page 160
LTL Model Checking......Page 161
From Mechanical to Solid State Disks......Page 162
Hashing......Page 163
Mapping......Page 164
Compressing......Page 166
Flushing......Page 167
I/O Efficient Model Checking with Solid State Disks......Page 168
Experimental Evaluation......Page 169
Conclusions......Page 172
Introduction......Page 175
Overview of the Methodology......Page 176
Informal Analysis Phase......Page 177
Example of Informal Analysis......Page 178
Formalization Phase......Page 179
Formal Validation Phase......Page 182
Overview of the Support Tools......Page 186
Discussion of the Approach......Page 187
Conclusions......Page 188
Introduction......Page 191
The Rewriting Logic Semantics of Java......Page 193
An Information-Flow Rewriting Logic Semantics for Java......Page 196
The Abstract Rewriting Logic Semantics of Java......Page 200
Experiments......Page 203
Related Work......Page 204
Conclusion......Page 205
Introduction......Page 208
Verification of the PRISE Safety Procedure: Aim and Approach......Page 209
The Primary-to-Secondary Leaking Fault Event......Page 210
The Implemented PRISE Safety Procedure......Page 211
Coloured Petri Net Model of the PRISE Safety Procedure......Page 213
State Space Analysis of Coloured Petri Nets......Page 216
Analysis of the PRISE CPN by Model Checking......Page 220
Conclusions......Page 222
Introduction......Page 224
Datalog......Page 226
Parameterised Boolean Equation System......Page 228
Datalog Query Representation......Page 229
Instantiation to Parameterless BES......Page 231
Optimizations......Page 232
Application to JAVA Program Analysis......Page 234
Datalog-Based Program Analysis......Page 235
Datalog-Based Program Analyzer......Page 236
Conclusions and Future Work......Page 238
back-matter......Page 241