Formal methods for industrial critical systems : 18th International Workshop, FMICS 2013, Madrid, Spain, September 23-24, 2013 : proceedings

This book constitutes the thoroughly refereed conference proceedings of the 18th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2013, held in Madrid, Spain, in September 2013. The 13 papers presented were carefully selected from 25 submissions and cover topics such as design, specification, code generation and testing based on formal methods, methods, techniques and tools to support automated analysis, certification, debugging, learning, optimization and transformation of complex, distributed, dependable, real-time systems and embedded systems, verification and validation methods, tools for the development of formal design descriptions, case studies and experience reports on industrial applications of formal methods, impact of the adoption of formal methods on the development process and associated costs, application of formal methods in standardization and industrial forums. Formal Methods for Industrial Critical Systems Preface 5 Organization 7 Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-linear and Linear Analyses 14 1 Control-Command Software Focused Analyses to Address V&V and Certification Needs 14 2 State of the Art of Formal Methods 15 2.1 Abstract Interpretation 16 2.2 SMT-Based Verification Approaches 16 3 Running Example: Coupled Mass System Linear Controller behind Triplicated Inputs with Saturations 17 3.1 Controller Design 18 3.2 Safety Architecture 19 3.3 Need for Formal Specification 20 4 BIBO (Bounded Input Bounded Output) for the Control Core: The Need for Non-linear Invariants 20 5 BIBO Stability for the Triplex Voter: Linear Analysis 23 5.1 Triplex Voting Verification Challenges 23 5.2 HullQe: A Technique for Property Directed Invariant Generation 24 6 Composing Proofs 27 7 Tools 27 8 Concrete Outcomes and Future Works 28 References 28 HyRev: A Tool for the Automatic Generation of Real-Time Routines for Enabling Fail-Safe Control in a Class of Safety-Critical Embedded Systems Using Backwards Reachability Analysis 30 1 Introduction 30 2 Preliminaries 33 3 Results 35 4 TheHyRevTool 40 5 Discussion 42 References 44 An Outline Workflow for Practical Formal Verification from Software Requirements to Object Code 45 1 Introduction 45 2 Overall Ricardo Workflow within MBAT 46 3 Key Activities 48 3.1 Requirements Phase 48 3.2 Design 50 3.3 Code 52 3.4 Object Code 53 4 Relationship with ISO 26262 53 4.1 Overview of Standard and Workflow 53 4.2 ISO 26262 Guidance on Requirements Phase 54 4.3 ISO 26262 Guidance on Design Phase 54 4.4 ISO 26262 Guidance on Implementation Phase 55 4.5 ISO 26262 Guidance on Testing Activities 55 4.6 ISO 26262 Guidance on Formal Verification 56 5 Limitations 57 6 Future Work 57 7 Conclusions 58 References 59 Boolean Quantifier Elimination for Automotive Configuration – A Case Study 61 1 Introduction 61 2 Preliminaries 62 3 Applications in Automotive Configuration 63 3.1 Automotive Configuration 63 3.2 Application 1: Model Counting on Customer-Relevant Options 66 3.3 Application 2: Projection of BOM Constraints 66 4 Existential Boolean Quantifier Elimination 67 4.1 Model Enumeration with Projection (MEP) 68 4.2 Model Enumeration and Generation of Shortest Prime Implicants (MEPI) 68 4.3 Variable Elimination by Clause Distribution (CD) 68 4.4 Substitute and Simplify (SS) 68 4.5 DNNF Computation and Projection (DNNF) 69 4.6 Quantifier Elimination by Dependency Sequents (DDS) 69 5 Benchmarks and Evaluation 69 5.1 Tools 70 5.2 Results 70 5.3 Evaluation in Terms of Our Applications 73 6 Conclusions and Outlook 74 References 74 Study on the Barriers to the Industrial Adoption of Formal Methods* 76 1 Introduction 76 2 Interview Process and Questions 77 3 Results 78 3.1 Use of Formal Methods 78 3.2 Barriers 79 3.3 Mitigations 83 4 Discussion 87 4.1 Cross-Correlations 87 4.2 Comparison with Prior Work and New Insights 87 5 Summary 88 References 89 On the Effectiveness of Assertion-Based Verification in an Industrial Context 91 1 Introduction 91 2 Effective ABV for PSL Assertions 92 2.1 Brief Overview of PSL 92 2.2 Hardware Monitors for PSL Assertions 93 2.3 Integration in EDA Tools 93 3 Case Study: HDLC Controller 94 3.1 Structure of the IP 94 3.2 Behavioural Description 95 4 HDLC Requirements in PSL 96 4.1 HDLC200. Transmitter: Sending Aborts 96 4.2 HDLC210. Receiver: Receiving Aborts 97 4.3 HDLC260. Receiving All Ones after Start 97 4.4 HDLC240. Transmitter Idle Mode 98 4.5 HDLC250. Transmitter Disabled before the End of a Frame 99 4.6 HDLC300. Transmitter: Ending a Frame 99 4.7 HDLC310. Receiver: Start of Frame Detection 100 4.8 HDLC320. Receiver: End of Frame Detection 101 4.9 HDLC160. Transmitter: Transparency 101 5 Characteristics of theMonitors 103 5.1 Synthesis 103 5.2 Gate Level Simulation and Power Consumption Analysis 104 6 Conclusions 104 References 105 Complex Digital System Design: A Methodology and Its Application to Medical Implants 107 1 Introduction 107 2 The HILECOP Methodology 108 2.1 Formal Definition of IPrTPN 109 2.2 Semantics of IPrTPN 110 2.3 HILECOP-Components 111 2.4 Automatic Generation of the VHDL Code 111 3 Use of Analysis in HILECOP Methodology 113 3.1 Formal Verification of System’s Properties 114 3.2 Handling Effective Conflicts 115 3.3 Finding Maximal Marking of Each Place 116 3.4 Determining the Number of Necessary Counters 117 4 Application on an Industrial System 117 4.1 Description of a Distributed Stimulation Unit (DSU) 117 4.2 DSU Model 118 4.3 Results Obtained 118 5 Conclusion 120 References 120 Formal Analysis of the ACE Specification for Cache Coherent Systems-on-Chip 121 1 Introduction 121 2 System Level Cache Coherency with ACE 122 2.1 ACE 123 2.2 ACE States 123 2.3 ACE Ports and Channels 123 2.4 ACE Transactions 124 3 Formally Modeling an ACE-Compliant SoC in CADP 126 3.1 Types and Data Structures 127 3.2 Channels 127 3.3 ACE Slave: Shared Memory 128 3.4 ACE Masters 129 3.5 ACE-Lite Masters 129 3.6 Cache Coherent Interconnect (CCI) 129 3.7 Requirements on the Global Ordering of Transaction 130 3.8 State Space Generation 130 4 Validation 131 4.1 Complete Execution of Transactions 131 4.2 Cache Coherency 132 4.3 Data Integrity 132 4.4 Model-Checking Results 133 5 Related Work 133 6 Conclusion 134 References 134 Predicate Abstraction for Programmable Logic Controllers 136 1 Introduction 136 1.1 Model Checking PLC Programs 136 1.2 Contribution and Outline 137 2 WorkedExample 137 3 Encoding of PLC Semantics in FOL 138 3.1 Encoding of Variables and the Program 138 3.2 From PLC Programs to FOL Formulae 140 3.3 Encoding of Timers 142 3.4 Summarization of Control-Flow Automata 143 4 Predicate Abstraction 144 4.1 Predicate Abstraction with Arcade.PLC 144 4.2 Scoping of Predicates 146 5 Case Study 147 6 Related Work 149 7 Conclusion 149 References 150 High-Level Guidance for Managers Deploying Formal Methods in Their Organisation 152 1 Introduction 152 2 A Method for Collecting and Presenting Evidence 154 3 Manager Scenarios Exploiting Shared Evidence Material 156 4 High-Level Guidance to Manager for FM Adoption 158 4.1 Overview 158 4.2 What Is the Impact on the Process and People Involved? 158 4.3 Can the Use of a Formal Method Be Hidden From Most of 161 4.4 What Strategy Increases the Chance of FM Adoption? 162 5 Related Work 163 6 Conclusion and Perspectives 164 References 165 Auditing User-Provided Axioms in Software Verification Conditions 167 1 Introduction 167 1.1 Use of Verification Conditions 167 1.2 The Need for Axioms 167 1.3 Problems with Using Axioms 169 1.4 Formal Support for Auditing Axioms 169 2 Related Work 170 3 Framework for Investigations 171 3.1 The SPARK Language 171 3.2 The SPARK Formal Verification Tool-Set 171 3.3 The Victor VC Translator and Prover Driver 172 4 Axiom Analysis 172 4.1 Exploring Properties of Axioms 172 4.2 Finding Minimal Sets of Axioms 174 4.3 Resolving Ambiguities in Axioms 175 5 Experimental Results 176 5.1 General Setup 176 5.2 Case Study 1: Tokeneer ID Station 176 5.3 Case Study 2: Mixed Floating-Point and Integer Arithmetic 179 6 Discussion 179 7 Conclusions and Future Work 180 References 181 Formal Reliability Analysis of Protective Relays in Power Distribution Systems 182 1 Introduction 182 2 Related Work 185 3 Modeling Relay-Based Protected Components 185 4 Verification of Reliability Properties 189 4.1 The PRISM Model Checker 189 4.2 Reliability Properties 190 5 Case Study: A Power Distribution Substation 191 6 Conclusion 194 References 195 Specification and Verification Using Alloy of Optimistic Access Control for Distributed Collaborative Editors 197 1 Introduction 197 2 Optimistic Access Control Protocol for DCE 199 2.1 Generation of Local Cooperative Requests 199 2.2 Reception of Remote Cooperative Requests 200 2.3 Generation of Administrative Operations 200 2.4 Reception of Remote Administrative Requests 201 2.5 Verification Issues 201 3 Specification and Verification 202 3.1 Alloy 203 3.2 Formal Specification of ACP 203 3.3 Specification of Consistency Property 207 4 Related Work 209 5 Conclusion 209 References 210 Author Index 212 Front Matter....Pages - Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-linear and Linear Analyses....Pages 1-16 HyRev: A Tool for the Automatic Generation of Real-Time Routines for Enabling Fail-Safe Control in a Class of Safety-Critical Embedded Systems Using Backwards Reachability Analysis....Pages 17-31 An Outline Workflow for Practical Formal Verification from Software Requirements to Object Code....Pages 32-47 Boolean Quantifier Elimination for Automotive Configuration – A Case Study....Pages 48-62 Study on the Barriers to the Industrial Adoption of Formal Methods....Pages 63-77 On the Effectiveness of Assertion-Based Verification in an Industrial Context....Pages 78-93 Complex Digital System Design: A Methodology and Its Application to Medical Implants....Pages 94-107 Formal Analysis of the ACE Specification for Cache Coherent Systems-on-Chip....Pages 108-122 Predicate Abstraction for Programmable Logic Controllers....Pages 123-138 High-Level Guidance for Managers Deploying Formal Methods in Their Organisation....Pages 139-153 Auditing User-Provided Axioms in Software Verification Conditions....Pages 154-168 Formal Reliability Analysis of Protective Relays in Power Distribution Systems....Pages 169-183 Specification and Verification Using Alloy of Optimistic Access Control for Distributed Collaborative Editors....Pages 184-198 Back Matter....Pages -