FORMS/FORMAT 2010: Formal Methods for Automation and Safety in Railway and Automotive Systems

3.3 Correction-Based Debugging......Page 5
 References......Page 9
Cover......Page 1
 2 Diagnosis Model......Page 2
 2 Rewriting of IL Programs Into SSA Form......Page 3
  3.1 Static Analysis......Page 4
Preface......Page 6
 5 Discussion & Future Work......Page 7
Invited Lectures......Page 13
 Achieving Europe-wide safety through technical harmonization......Page 14
 3 Proposal: Free / Libre Open Source Software for ETCS......Page 15
  1 Introduction......Page 16
   1.1 From National Diversity to European Standard......Page 17
   1.2 ETCS: A new Challenge for Europe’s Railways......Page 18
   2.1 Impact of “Closed Source” Software......Page 20
   2.2 Software Quality Issues in ETCS Projects......Page 21
   2.3 Quality Deficiencies in Software Products......Page 22
  3.7 How to Phase-in an OSS Approach into a ProprietaryEnvironment?......Page 26
   2.5 New Technologies Have to Have “At Least Same Level ofSafety”......Page 28
   2.6 Changing Business Model for Software: From Sales to Service......Page 29
  3 Proposal: Free / Libre Open Source Software for ETCS......Page 30
   3.2 ETCS Vehicle On-Board Units with “openETCS”......Page 32
  4.2 Industrial Software......Page 8
 5 Conclusions......Page 11
 References......Page 12
Table of Contents......Page 10
   1.3 Technology is not the Limiting Factor......Page 19
   2.4 Life Cycle of Complex Software......Page 24
   3.1 Public License for an “European” Project......Page 31
   3.3 Tools and Documents Need to be Included......Page 33
   3.4 “Open Proof” the ultimate Objective for openETCS......Page 35
   3.5 Formal Methods to validate Specification for openETCS......Page 36
   3.6 How FLOSS can meet Safety and Security Requirements......Page 37
   3.7 How to Phase-in an OSS Approach into a ProprietaryEnvironment?......Page 41
   3.8 Economical Aspects of openETCS for Europe’s Railway Sector......Page 43
   3.10 Benefits for Operators and Vehicle Owners......Page 44
  4 Conclusion......Page 45
  References......Page 47
 Formal Method and its Application on Train Operation Control System of Chinese high-speed Railway......Page 50
  1 Overview......Page 51
1st Day Sessions......Page 53
  1 Introduction......Page 54
  2 Modeling Human Behaviour......Page 56
  3 Modeling the Impact of Human Behavior on Safetyand Security of the Transportation Process......Page 59
  4 Conclusion......Page 60
  References......Page 61
  1 Introduction......Page 63
   3.1 What is RAMS?......Page 64
   3.2 Problems in failure verification related to railway signalling system in JR East......Page 65
   3.3 Importance of reliability management......Page 66
   3.5 Analysis result......Page 68
  4 Conclusion......Page 71
  1 Introduction......Page 72
  2 Technical presentation of the TC and the AC......Page 73
  3 Functional differences and specific Constraints......Page 74
  4 Modelling......Page 76
  5 Conclusions......Page 82
  References......Page 83
  1 Introduction......Page 84
  2 Theoretical basis......Page 85
  3 Case study......Page 88
  References......Page 92
  1 Introduction......Page 93
  2 System Architecture......Page 95
  3 Modeling Dispatching Systems......Page 98
  4 Conclusion......Page 100
  2 Railway Signalling System and RAMS Indicators......Page 102
   3.1 Basic Concepts......Page 103
   3.2 Method to Estimate the Loss Caused by Failures......Page 104
   4.1 Preconditions......Page 105
  5 Conclusion......Page 109
  1 Introduction......Page 111
  2 Interlocking Systems Representation......Page 112
  3 Safety Requirements......Page 113
  4 NuSMV......Page 114
  5 SPIN......Page 115
  References......Page 118
  1 Introduction......Page 120
   2.2 Network......Page 121
   2.3 Field Controller (FC)......Page 122
  4 Problem of the IP Network-based Signal Control System......Page 123
  6 Reliability of the Integrated Logical Controller......Page 125
  7 Conclusion......Page 127
  1 Introduction......Page 128
   2.1 Definition and frequency......Page 129
   3.1 To monitor axle boxes by train staff......Page 130
   3.3 To monitor axle boxes by on track HBD......Page 131
   4.1 Evaluation of sub-functions and activities......Page 133
   4.2 Application on a high speed line......Page 135
  5 Conclusion......Page 136
  1 Introduction......Page 137
   2.1 BP-Risk......Page 138
   2.2 System definition......Page 139
   2.4 Consequence analysis......Page 140
  3 THR Derivation......Page 143
  4 Conclusion......Page 144
  1 Introduction......Page 146
  3 Subsystem Design and Formal Specification with ACSL......Page 148
   3.2 Using ACSL......Page 149
  5 Results of Deductive Verification......Page 151
  6 Conclusions and Future Work......Page 152
  Acknowledgments......Page 153
  1 Introduction......Page 155
  2 Modeling of the Basic Parallel Hybrid Structure......Page 156
   2.1 Forward and Backward Calculation on the Vehicle......Page 157
   2.2 Hybrid and Non-Hybrid operating Modes......Page 158
  3 Parametrization of Optimality Criteria......Page 159
   4.1 Heuristic Hybridization Strategy......Page 160
   4.2 Optimized Operating Strategy......Page 161
  5 Conclusions and Outlook on Future Research......Page 162
  References......Page 164
2nd Day Sessions......Page 165
  1 Introduction......Page 166
   2.1 How should the requirements from the CSM Regulation befulfilled......Page 167
   2.2 Significant change......Page 168
   2.3 Hazard Record......Page 169
   2.4 Tools and Methods for risk assessment......Page 171
  3 Conclusions and outlook......Page 172
  References......Page 173
  1 Introduction......Page 174
   3.1 Motivation......Page 175
   3.2 System Definition and Application Conditions......Page 176
   3.4 System Requirements......Page 177
  4 Example of a Newly Constructed Risk Graph......Page 178
  5 Conclusion......Page 180
  References......Page 182
  1 Introduction......Page 183
  3 System Definition......Page 184
  4 Severity Classification......Page 185
  5 Assessment of Accident Scenarios......Page 187
  7 Examples......Page 189
  References......Page 190
  1 Introduction......Page 192
  2 Simulation Platform......Page 193
  3 Property Specification......Page 195
  4 Online Evaluation of LTL formulas......Page 196
  5 Guided Simulation by Exploring the Behaviour Spectrum......Page 199
  6 Summary......Page 201
  1 Introduction......Page 203
   1.2 Structure of the Paper......Page 204
   2.1 Interweaving Development Streams......Page 205
   2.3 Semantic Reasoning......Page 206
  3 Example Application and Prototype Toolchain......Page 207
  4 Lessons Learned from Applying Semantic Reasoning......Page 209
  5 Conclusion......Page 210
  1 Introduction......Page 212
  2 A system model to traffic modelling......Page 213
  3 Requirements for investigation of TAS......Page 214
  5 Two-level approach for calibration and validation......Page 215
  6 Data acquisition concept......Page 216
  7 Empirical Results......Page 218
  8 Conclusion......Page 219
  References......Page 220
  1 Introduction......Page 221
  2 Architecture of the Tool Integration Framework......Page 223
  3 Implementation of the Tool Integration Framework......Page 225
  4 Case Study: Model-based Test Case Generation......Page 226
  5 Conclusions......Page 228
  1 Introduction......Page 230
  2 Rewriting of IL Programs Into SSA Form......Page 232
  3 Generation of Invariants......Page 233
  4 Related Work......Page 236
  References......Page 237
  1 Introduction......Page 239
  2 Diagnosis Model......Page 240
   3.1 Static Analysis......Page 242
   3.3 Correction-Based Debugging......Page 243
   4.1 Case Study......Page 244
   4.2 Industrial Software......Page 246
  References......Page 247
Author Index......Page 249