Formal methods for industrial critical systems : 19th International Conference, FMICS 2014, Florence, Italy, September 11-12, 2014 : proceedings

This book constitutes the proceedings of the 19th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2014, held in Florence, Italy, in September 2014. The 13 papers presented in this volume were carefully reviewed and selected from 26 submissions. They are organized in topical sections named: cyber-physical systems; computer networks; railway control systems; verification methods; and hardware and software testing. Formal Methods for Industrial Critical Systems Preface 5 Organization 7 20 Years Past and (Hopefully) 20 Yearsto Come: My Experience in Ansaldo STSwith Formal Methods and Railways 10 Quantitative Verification:Formal Guarantees for Timeliness,Reliability and Performance 11 Table of Contents 12 Formal Verification of Steady-State Errorsin Unity-Feedback Control Systems 14 1 Introduction 14 2 Related Work 17 3 Preliminaries 18 3.1 Multivariate Calculus Theories in HOL-Light 18 3.2 Formalization of Block Diagrams in Control Systems 19 4 Steady-State Error Analysis 22 5 Application: Pulse Width Modulation (PWM) push-pull dc-dc Converter 24 6 Conclusions 27 References 27 Assertion-Based Monitoring in Practice –Checking Correctnessof an Automotive Sensor Interface 29 1 Introduction 29 2 Verification Flow in the Automotive Domain – State-of-the-Practice 31 3 Signal Temporal Logic 33 4 Case Study 35 4.1 Case Study Description 35 4.2 Formalization of DSI3 Discovery Mode Requirements 36 4.3 Case Study Evaluation 40 5 Lessons Learned and Future Directions 42 6 Conclusions 43 References 43 Formal Analysis of a Fault-Tolerant RoutingAlgorithm for a Network-on-Chip 61 1 Introduction 61 2 Related Work 62 3 Network-on-Chip Architecture and Routing Algorithm 63 4 Formal Models of NoCs 65 4.1 One Direction Routing 65 4.2 Removing Arbiter’s Buffering Ability 67 4.3 Finding Proper Data Abstractions 68 5 Verification Results 70 6 Discussion 73 References 74 Formal Specification and Verificationof TCP Extended with the Window Scale Option 76 1 Introduction 76 2 Related Work 77 3 Specification 78 3.1 The TCP Instance 80 3.2 The Complete System 84 4 Verification 85 5 Conclusion 89 References 89 Learning Fragments of the TCP Network Protocol 91 1 Introduction 91 2 The TCP Network Protocol 92 3 Regular Inference Using Abstraction 94 3.1 Learning Mealy Machines 94 3.2 Inference Using Abstraction 95 4 Learning Setup 96 5 Messages and Abstraction 97 5.1 Mapper Description 97 5.2 Initial State Detection 100 6 Complications Encountered 101 7 Experimental Results 103 8 Concluding Remarks and Future Work 105 References 105 On the Validation of an Interlocking Systemby Model-Checking 107 1 Introduction 107 2 Ladder Logic Diagrams 108 3 VerificationGoals 111 4 Environment Assumptions and Slicing 112 5 CEGAR-Like Verification Process 114 6 Model Extraction 116 7 Verification with Design Verifier 117 8 Conclusion 119 References 120 An Open Alternative for SMT-Based Verification of SCADE Models 137 1 Introduction 137 2 Preliminaries 139 2.1 SCADE and SCADE DV 139 2.2 SatisfiabilityModulo Theories 140 2.3 Simplified SMT-Logic 140 2.4 Streams 141 3 TheLAMA Language 141 3.1 Dynamic Semantics 142 4 Translating SCADE to LAMA 144 5 Translating LAMA to SMT 146 5.1 SMT-Formulas from Nodes 146 5.2 Translating Dataflow 147 5.3 SMT-Formulas from Programs 148 5.4 Correctness of the Translations 148 6 Implementation and Experiments 148 6.1 Benchmarks 149 7 Conclusion and Future Work 151 References 151 Improving Static Analyses of C Programs with Conditional Predicates 153 1 Introduction 153 2 A Generic Abstract Interpretation Based Framework 155 3 Predicated Analyses 157 3.1 Predicated Domains 157 3.2 Abstract Transfer Functions 159 4 Improving the Analysis 161 4.1 Avoiding Redundant Values 161 4.2 Convergence of the Analysis and Practical Complexity 162 5 Applications 163 5.1 A First Abstract Domain: Initialized Variables 163 5.2 A Second Abstract Domain: Equalities 164 6 Experimental Results 165 7 Conclusion 166 References 167 Detecting Consistencies and Inconsistencies of Pattern-Based Functional Requirements 168 1 Introduction and Related Work 168 2 BTC Patterns 169 2.1 Base Pattern 170 2.2 Start-up Phase 170 2.3 Activation Modes 170 2.4 Example 171 3 Trace and Pattern Semantics 172 3.1 Traces and Formulas 172 3.2 Pattern Semantics 173 3.3 Specifications and Their Standard Semantics 174 3.4 Intended Specification Semantics 175 4 Consistency 176 4.1 Existential Consistency 176 4.2 Bounded Consistency 177 5 ToolIntegration 180 6 Conclusion and Future Work 181 References 181 Test Specification Patterns for Automatic Generation of Test Sequences 183 1 Introduction 183 2 Background 184 2.1 The CRYSTAL Project 185 2.2 V&V UML Profile and Test Sequence Generation 185 2.3 Specification Patterns 187 3 TSPs Definition and Implementation 187 4 Promela Code Generation 191 5 The Radio Block Centre Use Case 192 5.1 Application to RBC 193 6 Conclusions and Future Developments 195 References 196 Randomised Testing of a Microprocessor ModelUsing SMT-Solver State Generation 198 1 The Processor Model 200 2 Instruction Sequence Generation 201 2.1 Sanity Checks 202 3 Generating Pre-states for Testing 202 3.1 Additional Requirements 203 3.2 Practical HOL 204 3.3 Preparing for SMT Solving 205 4 Test Execution and Comparison 206 4.1 Scaling Up Testing 207 5 Outcomes from Testing 208 5.1 Performance 208 6 Discussion 209 7 Related Work 211 8 Conclusion 212 References 212 Author Index 213 Front Matter....Pages - Formal Verification of Steady-State Errors in Unity-Feedback Control Systems....Pages 1-15 Assertion-Based Monitoring in Practice – Checking Correctness of an Automotive Sensor Interface....Pages 16-32 Analysis of Real-Time Properties of a Digital Hydraulic Power Management System....Pages 33-47 Formal Analysis of a Fault-Tolerant Routing Algorithm for a Network-on-Chip....Pages 48-62 Formal Specification and Verification of TCP Extended with the Window Scale Option....Pages 63-77 Learning Fragments of the TCP Network Protocol....Pages 78-93 On the Validation of an Interlocking System by Model-Checking....Pages 94-108 Deadlock Avoidance in Train Scheduling: A Model Checking Approach....Pages 109-123 An Open Alternative for SMT-Based Verification of Scade Models....Pages 124-139 Improving Static Analyses of C Programs with Conditional Predicates....Pages 140-154 Detecting Consistencies and Inconsistencies of Pattern-Based Functional Requirements....Pages 155-169 Test Specification Patterns for Automatic Generation of Test Sequences....Pages 170-184 Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation....Pages 185-199 Back Matter....Pages -