NASA formal methods: 13th International Symposium, NFM 2021, virtual event, May 24-28, 2021 : proceedings /

This book constitutes the proceedings of the 13th International Symposium on NASA Formal Methods, NFM 2021, held virtually in May 2021. The 21 full and 3 short papers presented in this volume were carefully reviewed and selected from 66 submissions. The papers aim to identify challenges and provide solutions to achieve assurance in mission-critical and safety-critical systems. Examples of such systems include advanced separation assurance algorithms for aircraft, next-generation air transportation, autonomous rendezvous and docking of spacecraft, on-board software for unmanned aerial systems (UAS), UAS traffic management, autonomous robots, and systems for fault detection, diagnosis, and prognostics. Preface Organization Abstracts of Invited Talks SMT Solving: Past, Present, and Future The Flavour of Real-World Vulnerability Detection and Intelligent Configuration Distribution-aware Validation of Neural Networks Contents Balancing Wind and Batteries: Towards Predictive Verification of Smart Grids 1 Introduction 2 Preliminaries 3 Continuous-State Power System Modelling 3.1 Grid Model Dynamics 3.2 Grid Frequency Control 3.3 Ancillary Service Deployment 3.4 Discrete-Time Storage-Integrated Power System Model 4 Discrete-State Receding Horizon Control Problem 4.1 Stochastic Wind Power Model 4.2 State Space Exploration Procedure 5 Numerical Study 5.1 Experimental Setup 5.2 Results 6 Concluding Remarks References nnenum: Verification of ReLU Neural Networks with Optimized Abstraction Refinement 1 Introduction 2 Overview 2.1 Verification Problem 2.2 ACAS Xu Benchmarks 2.3 Set Representations 2.4 Verification Algorithm Overview 3 Optimizations 3.1 Zonotope Domain Contraction 3.2 Direct Abstraction Refinement 3.3 Abstraction Refinement Improvements 4 Related Work 5 Conclusion References Minimum-Violation Traffic Management for Urban Air Mobility 1 Introduction 1.1 Problem Significance 1.2 Scalable and Verifiable Safety for UAM 1.3 Setting 1.4 Contribution and Innovation 1.5 Path to Deployment 1.6 Related Work 2 Notation and Setting 2.1 Operating Environment 3 Problem Formulation 3.1 Problem Statement 4 Solution Approach 4.1 Overview 5 Experimental Results 6 Conclusion References Integrating Formal Verification and Assurance: An Inspection Rover Case Study 1 Introduction 2 Tool Support 3 Assurance-Based Formal Methods Integration 4 The Case Study Step-by-Step 4.1 Step 0: Characterize Initial System 4.2 Step 1: Create Initial System Model 4.3 Step 2: Perform Preliminary Hazard Analysis 4.4 Step 3: Define Mitigations and Safety Requirements 4.5 Step 4: Refine System Model According to Mitigations 4.6 Step 5: Formalize Requirements and Create Formal Specifications 4.7 Step 6: Perform Verification and Simulation at System- and Component-Levels 4.8 Step 7: Document Verification Results and Build Safety Case 5 Discussion 6 Related Work 7 Conclusions and Future Work References Towards Verifying SHA256 in OpenSSL with the Software Analysis Workbench 1 Introduction 2 Compositional Proofs for OpenSSL SHA256 3 Results and Conclusion References Polygon Merge: A Geometric Algorithm Verified Using PVS 1 Introduction 2 Polygon Merge 2.1 Classes of Polygons Supported 2.2 Vertex Injection 2.3 Edge Traversal and Selection 3 Correctness Requirements 3.1 Point Membership in Polygons 3.2 Top-Level Requirements 4 Formalization and Problem Domain 4.1 Formalization of Geometric Features 4.2 Key Algorithm Functions 4.3 Implementation in SPARK Ada 5 Proof Decomposition 5.1 Forward Point Containment 5.2 Reverse Point Containment 5.3 Well-Formedness of Merged Polygon 5.4 Merge Algorithm Commutativity 5.5 Equivalence of Point Membership Criteria 5.6 Supporting Lemmas 5.7 Problems Discovered 6 Related Work 7 Conclusion References Program Sketching Using Lifted Analysis for Numerical Program Families 1 Introduction 2 From Sketches to Program Families 2.1 Sketches 2.2 Program Families 2.3 Encoding of Sketches as Program Families 3 Synthesis by Lifted Analysis 3.1 Basic Lifted Analysis 3.2 Extended Lifted Analysis 3.3 Synthesis Algorithm 4 Evaluation 5 Related Work and Conclusion References Specification Decomposition for Reactive Synthesis 1 Introduction 2 Preliminaries 3 Modular Synthesis 4 Decomposition of Nondeterministic Büchi Automata 5 Decomposition of LTL Formulas 6 Experimental Evaluation 6.1 LTL Decomposition 6.2 Automata Decomposition 7 Conclusions References On Symmetry and Quantification: A New Approach to Verify Distributed Protocols 1 Introduction 2 Preliminaries 3 Protocol Symmetries 4 SymIC3: Symmetric Incremental Induction 5 Quantifier Inference 5.1 Basic Quantifier Inference 5.2 Quantifier Inference Beyond ** 6 Finite Convergence Checks 7 IC3PO: IC3 for Proving Protocol Properties 8 Evaluation 8.1 Results 8.2 Discussion 9 Related Work 10 Conclusions and Future Work References Integrating Runtime Verification into a Sounding Rocket Control System 1 Introduction 2 System Description 3 Approach 4 Runtime Specification Development 5 Results 6 Conclusion References Verification of Functional Correctness of Code Diversification Techniques 1 Introduction 2 System Overview 2.1 Disassembly 2.2 Control-Flow Graph Construction 2.3 Local Variable Normalization 2.4 CFG Comparison 2.5 Output 3 Soundness of Code Diversification 4 Algorithm 5 Evaluation 5.1 Results 5.2 Limitations 6 Past and Related Work 7 Conclusion References Scalable Reliability Analysis by Lazy Verification 1 Introduction 2 Boolean Logic-Driven Markov Processes 3 Lazy Probabilistic Verification 3.1 State-Space Generation 3.2 Lazy Verification 4 The Initiator and All Barriers Method 5 Case Studies 6 Results and Discussion 6.1 Accuracy 6.2 Computation Time 6.3 Gained Insights on Lazy Verification 7 Conclusion References Robustifying Controller Specifications of Cyber-Physical Systems Against Perceptual Uncertainty 1 Introduction 2 Controller-Plant Models in Event-B 3 Uncertainty Injection 4 Robustification 4.1 Types of Robustified Events 4.2 Action-Preserving Robustification 4.3 Action-Repurposing Robustification 4.4 Checking Vacuity of Heterogeneous Events 5 Implementation 6 Case Study 7 Related Work 8 Conclusion References Good Fences Make Good Neighbors 1 Introduction 2 Prior Work 3 Provably Safe Remediation Maneuvers 3.1 Geofence Representation 3.2 Euler Spiral Turns 3.3 Determining Euler Spiral Turn Safety 3.4 Arbitrary Initial Conditions 3.5 Computational Efficiency 4 Extensions to Nondeterministic Trajectories 5 Application 6 Conclusions and Future Work References Online Shielding for Stochastic Systems 1 Introduction 1.1 Related Work 2 Preliminaries 3 Setting and Problem Statement 4 Online Shielding for MDPs 4.1 Behaviour Models for Adversaries 4.2 Safety-Relevant MDP M 4.3 Sub-MDP M for Next Decision 4.4 Shield Construction 4.5 Optimisation – Updating Shields After Adversary Decisions 5 Implementation and Experiments 6 Conclusion and Future Work References Verification of Eventual Consensus in Synod Using a Failure-Aware Actor Model 1 Introduction 2 The Synod Protocol 2.1 Progress in Synod 3 A Failure-Aware Actor Model 4 Formal Verification of Eventual Progress in Synod 4.1 Fairness Assumptions for Transitions 4.2 Rules Specifying the Actions of Synod Actors 4.3 Assumptions About the Future Behavior of Agents 4.4 The Proof of Progress 5 Related Work 6 Conclusion References An Infrastructure for Faithful Execution of Remote Attestation Protocols 1 Introduction 2 Virus Checking as Attestation 3 Copland Language and Reference Semantics 3.1 Copland Phrases 3.2 Concrete Evidence 3.3 Copland LTS Semantics 4 Copland Compiler and Virtual Machine 5 Verification 5.1 Lemmas 5.2 Automation 6 Attestation Manager(AM) Monad 7 Related Work 8 Future Work and Conclusion References Verifying Min-Plus Computations with Coq 1 Problem Statement 2 Notations 3 (min, plus) Operators on Functions 3.1 (min, plus) Operators 3.2 Sub-classes of Functions for Effective Computation 4 State of the Art 5 Ultimately Pseudo Periodic Functions 6 UPP and Piecewise Affine Functions 7 Stability of UPP Functions by (min, plus) Operators 8 Stability of UPP-PA Functions by (min, plus) Operators 9 Finite Equality Criteria on UPP-PA 10 Implementation 11 Conclusion References Efficient Verification of Optimized Code 1 Introduction 1.1 Contributions 1.2 Availability of Results 2 Elliptic Curve Cryptography on Small Devices 2.1 Curve25519 2.2 X25519 on AVR 3 Why3 Verification Platform 4 Correctness of Low-Level Code 4.1 A Re-Usable Validated AVR Machine Model 4.2 Proving the Correctness of AVR Assembly Code 5 Correctness of the C Code 5.1 Verifying the Montgomery Ladder 5.2 A Succinct Specification of X25519 6 Improved X25519 for AVR 6.1 Memory Safety 6.2 Interrupt Safety 7 Related Work 8 Conclusion References A Formal Proof of the Lax Equivalence Theorem for Finite Difference Schemes 1 Introduction 2 Lax Equivalence Theorem 2.1 Consistency, Stability and Convergence 2.2 Formalization in the Coq Proof Assistant 3 Proof of Consistency of a Sample Finite Difference Scheme 3.1 Proof of Consistency for the Finite Difference Scheme 3.2 Formalization in the Coq Proof Assistant 3.3 Relating Pointwise Consistency to the Lax Equivalence Theorem 3.4 Formalization in Coq 4 Stability of the Scheme 4.1 Lemma to Verify that the Eigenvalues and Eigenvectors Belong to the Spectrum of Ah(a,b,a) 4.2 Lemma on the Boundedness of the Matrix Norm for Scheme Nh 4.3 Main Stability Theorem 5 Application of the Lax Equivalence Theorem to the Example Problem 6 Conclusion and Future Work 6.1 Effort and Challenges References Recursive Variable-Length State Compression for Multi-core Software Model Checking 1 Introduction 1.1 Related Work 1.2 Contributions 2 Tree Compression 2.1 TreeDBS and Its Implementation 3 Dtree 3.1 A Chain of Perfectly Balanced Binary Trees 3.2 Incremental Updates 3.3 Partial Reconstruction of States 3.4 Determining a State Is New 4 DMC Model Checker 4.1 An Example Using a Tree of States 5 Experiments 5.1 Variable-Length State Models 5.2 Fixed-Length State Models 6 Discussion and Conclusion 6.1 Future Work References Runtime Verification of Generalized Test Tables 1 Introduction 2 Generalized Test Tables 2.1 Syntactical Elements 2.2 Semantics: Table Conformance 2.3 Automaton Generation 3 Monitor Generation 3.1 Global Parameters and Nondeterminism 3.2 Combined Monitors 3.3 Triggered Restarts and Dynamic Monitors 4 Application Scenarios 4.1 Cruise Control System 4.2 Linear Regression 4.3 Conveyor Belt Process 5 Discussion: Generalizations 6 Related Work 7 Conclusion References Quasi-Equal Clock Reduction On-the-Fly 1 Introduction 2 Preliminaries 2.1 Clocks, Zones, and Difference-Bound-Matrices 2.2 Networks of Timed Automata 2.3 Quasi-Equal Clocks 3 DBMT: DBMs with Clock Partitions and Tokens 4 Standard Operations on DBMx 5 Splitting and Merging Equivalence Classes 6 Putting It All Together 7 Evaluation 8 Conclusion References On the Effectiveness of Signal Rescaling in Hybrid System Falsification 1 Introduction 2 Preliminary 3 A Rescaling Approach for Tackling the Scale Problem 4 Experimental Evaluation 5 Conclusion and Future Work References Author Index