NASA Formal Methods

Name: NASA Formal Methods | 16th International Symposium, NFM 2024, Moffett Field, CA, USA, June 4-6, 2024, Proceedings
Brand: Springer
Price: 128.39 EUR
Availability: OnlineOnly

16th International Symposium, NFM 2024, Moffett Field, CA, USA, June 4-6, 2024, Proceedings

Nathaniel Benz Divya Gopinath Nija Shi(Herausgeber*in)

Springer (Verlag)

Erschienen am 27. Mai 2024

XXIII, 438 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-031-60698-4 (ISBN)

128,39 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Intro
Preface
Organization
Abstracts of Invited Talks
Autonomy Challenges for Future NASA Science and Exploration Missions
Formal Verification and Run-time Monitoring for Learning-Enabled Autonomous Systems
Safety Under Uncertainty: Automotive Standards for AI Safety and Research Perspectives
Contents
Advances in Solver Technology
Structure-Guided Cube-and-Conquer for MaxSAT
1 Introduction
1.1 Our Contributions
2 Preliminaries
2.1 Structure of Propositional Formulas
3 Inprocessing with Torso Decompositions
3.1 Graph Torsos and Torso Decompositions
3.2 Computing Torso Decompositions
3.3 Structure-Guided Inprocessing
3.4 Soundness and Completeness
4 Experimental Evaluation
4.1 Decomposing Large Formulas
4.2 Improving MaxSAT Solvers with Structure-Guided Inprocessing
4.3 Limitations of Structure-Guided Cube-and-Conquer
5 Conclusion and Further Research
References
Tackling the Polarity Initialization Problem in SAT Solving Using a Genetic Algorithm
1 Introduction
2 Basic Definitions and Technical Background
2.1 Boolean Satisfiability
2.2 Complete and Incomplete Algorithms
2.3 Genetic Algorithms
3 Related Works
3.1 IPP Methods and Heuristics
3.2 Genetic Algorithms in SAT Solving
4 Tackling IPP with GA
4.1 Description of Genetic Algorithm for SAT Polarity Initialization (gaspi)
4.2 Configuration of GASPI Parameters
5 Experimental Results
5.1 Solvers
5.2 Benchmarks
5.3 Results
6 Conclusion and Future Works
References
Formalization of Asymptotic Convergence for Stationary Iterative Methods
1 Introduction
2 Overview of Stationary Iterative Methods
3 Generic Iterative Convergence Theorem in the Field of Reals
4 Formalization of the the Generalized Iterative Convergence Theorem (Theorem 1) in Coq
4.1 Formalizing Properties of Complex Matrices and Vectors
4.2 Formalization of Vector and Matrix Norms
4.3 Formalization of the Theorem 1 in Coq
5 Proof of Convergence for the Gauss-Seidel Method
5.1 Formalization of Easily Checkable Conditions
5.2 Proof of Convergence for the Gauss-Seidel Method
6 Model Problem
6.1 Gauss-Seidel Method
6.2 Jacobi Method
7 Related Work
8 Conclusion and Future Work
References
Distributional Probabilistic Model Checking
1 Introduction
1.1 Related Work
2 Background
2.1 Random Variables and Probability Distributions
2.2 Markov Chains and Markov Decision Processes
3 Distributional Probabilistic Model Checking
4 Distributional Model Checking Algorithms
4.1 Forward Distribution Generation for DTMCs
4.2 Risk-Neutral Distributional Value Iteration for MDPs
4.3 Risk-Sensitive Distributional Value Iteration for MDPs
5 Experiments
5.1 Case Studies
5.2 Results Analysis
6 Conclusion
References
Formal Methods for Program Analysis and Verification
Quantitative Input Usage Static Analysis
1 Introduction
2 Overview
3 Quantitative Input Data Usage
4 A Static Analysis for Quantitative Input Data Usage
5 Experimental Results
6 Related Work
7 Conclusion
References
Verifying a C Implementation of Derecho's Coordination Mechanism Using VST and Coq
1 Introduction
2 Background on Derecho, Coq, and VST
3 The SST Interfaces: Code API and Trace-Based Specs
4 Example: Stability Detection
5 The SST Implementation and Its Verification
6 Example: Distributed Transitive Closure
7 Related and Future Work
References
Verification of Scapegoat Trees Using Dafny
1 Introduction
2 Background
2.1 Scapegoat Trees
2.2 Balance Properties
2.3 Rebuild and Rebalance
2.4 Dafny
3 Implementation
3.1 Basics
3.2 Insert
3.3 Delete
3.4 Verification Result
4 Discussions
4.1 Issues
4.2 Proof Techniques
5 Proof Example: Sequence_Properties
6 Conclusion
References
Real Arithmetic in TLAPM
1 Introduction
2 Enabling Real Arithmetic in the TLA+ Proof Manager
2.1 Typed Encodings
2.2 Untyped Encodings
3 Safety Verification of Cyber-Physical Systems
4 Conclusion
References
SMT-Based Assurance of Behavioral Specifications
Deductive Model Refinement
1 Introduction
2 Preliminaries
2.1 Required Properties
2.2 Behavioral Models
2.3 Specification and Refinement
3 Model Refinement as Constraint Solving
4 Function Synthesis
5 Path Properties
5.1 Algorithm Design Example: Sorting
6 Related Work
7 Concluding Remarks
References
Symmetry-Based Abstraction Algorithm for Accelerating Symbolic Control Synthesis
1 Introduction
2 Preliminaries
2.1 System and Problem Definitions
2.2 Transformation Groups and Equivariant Control Systems
2.3 Cartan's Moving Frame and Computing Lower-Dimensional Reachsets
2.4 Discrete Abstractions of Continuous-Time Control Systems
2.5 Discrete Control Synthesis
2.6 Symmetry-Based Discrete Transitions Computation
3 Symmetry-Based Abstraction
4 Symmetry-Based Control Synthesis Algorithm
5 Case Study
6 Conclusions
A Proof of Corollary 1
B Specification Correspondence Between a Continuous-Time System and a Corresponding Discrete Abstraction
C Details of the Ship-Docking Case Study
References
SMT-Based Aircraft Conflict Detection and Resolution
1 Introduction
2 SMT-Based Conflict Detection and Resolution
2.1 Generating Valid Candidate Flight Plans
2.2 Analyzing the Generated Candidates for Conflict
3 Simulations
3.1 Simulated Example
3.2 Performance Benchmarking
4 Discussion
5 Related Work
6 Conclusion
References
Formal Methods for Learning-Enabled Systems
Towards Formal Verification of Neural Networks in Cyber-Physical Systems
1 Introduction
2 Related Works
3 Background
3.1 PVS Language
3.2 Neural Network
3.3 PyTorch
4 Translation of Neural Networks to Formal Models
4.1 Network Constraints and Properties
4.2 Linking PVS and PyTorch Together
5 Use Case: Adaptive Cruise Control with MPC
5.1 Modelling and Proving Properties for the Neural Network
6 Conclusions
A Proving the Type-Checking Constraints (TCCs)
B Dealing with Transcendental Activation Functions
References
Approximate Conformance Verification of Deep Neural Networks
1 Introduction
2 Conformance Checking of Neural Networks
2.1 Preliminaries
3 Conformance Checking Algorithm
3.1 Append Hidden Layer
3.2 Merge Networks
3.3 Reachability-Based Approach for the Conformance Checking
4 Implementation and Experiments
5 Application of Conformance Checking to Closed-Loop Systems
5.1 Case Study: Automatic Rocket Landing System
6 Related Works
7 Conclusion
References
Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems
1 Introduction
2 Preliminaries and Problem Statement
3 Our Approach
3.1 Our Approach: Compositional Method
3.2 Automatic Inference of Generalized Bridge Predicates
3.3 Heuristic for Falsifying Inductiveness
3.4 Algorithm
4 Evaluation
4.1 Implementation and Experimental Setup
4.2 Case Studies and Experimental Results
5 Related Work
6 Conclusions
References
Formal Methods for Automotive Systems
Tree-Based Scenario Classification
1 Introduction
2 Motivational Example
3 A Temporal Logic for Properties of Scenarios
4 Classifiers for Scenarios and Metrics on Sets of Scenarios
4.1 Classifiers for Scenarios
4.2 Coverage Metrics for Sets of Scenarios
5 Evaluation
5.1 Discussion
5.2 Threats to Validity
6 Conclusion
References
Validation of Reinforcement Learning Agents and Safety Shields with ProB
1 Introduction and Motivation
2 Background
3 Formal Models for Reinforcement Learning Agents
3.1 Creation of the Formal Model
3.2 Implementing a Safety Shield around the RL Agent
3.3 Validatability and Verifiability
4 Case Study
4.1 Formal B Model for Highway Environment
4.2 Training the Agents
4.3 Statistical Validation
4.4 Validation by Trace Replay
5 Related Work
6 Conclusion and Future Work
References
Contract-Driven Runtime Adaptation
1 Introduction
2 Motivating Example
3 Preliminaries
4 Adaptive Contracts
5 Runtime Adaptation Framework
6 Case Study
7 Related Work
8 Limitations and Future Work
References
Topllet: An Optimized Engine for Answering Metric Temporal Conjunctive Queries
1 Introduction
2 Background
3 Topllet
4 Performance
5 Conclusion and Future Work
References
A Formal Verification Framework for Runtime Assurance
1 Introduction
1.1 Runtime Assurance
1.2 Plaidypvs
2 RTA Framework in Plaidypvs
3 A Simple Example
4 Conclusion
References
Formal Methods for Robotics
SMT-Based Dynamic Multi-Robot Task Allocation
1 Introduction
2 Related Work
3 Problem Formulation
3.1 Workspace Model
3.2 System Model
3.3 Problem Statement
4 Summary of Approach
4.1 Preliminaries
4.2 Encoding Literals
4.3 Incremental Solving
4.4 SMT Encoding
4.5 Overall Algorithm
5 Theoretical Results
5.1 Soundness
5.2 Completeness
6 Experimental Analysis
6.1 RQ1: Performance of Initial Solve and Comparison on Theories
6.2 RQ2: Performance of Incremental Solve
7 Conclusion and Future Work
References
Control Barrier Function Toolbox: An Extensible Framework for Provable Safety
1 Introduction
2 Background
3 Organization
4 Software Example
5 Hardware Experiment
6 Conclusion
References
Robotics: A New Mission for FRET Requirements
1 Introduction
2 Systematic Review: Identification of Robotic Patterns
2.1 Methodology: Systematic Review
2.2 Answering the Research Questions
3 Expressing Robotic Missions in FRET
4 Discussion
4.1 Expressibility of FRETish for Robotic Mission Requirements
4.2 Comparing Patterns with FRETish Robotic Requirements in the Wild
4.3 On PsALM and FRET
4.4 Threats to Validity
5 Related Work
6 Conclusion
References
Safe Planning Through Incremental Decomposition of Signal Temporal Logic Specifications
1 Introduction
2 Motivation
3 Preliminaries
4 Approach
4.1 Basic Concepts and Definitions
4.2 Flattening
4.3 Symbolic Time Resolution
4.4 Scheduling
5 Evaluation
5.1 Experimental Setup
5.2 Results
6 Related Work
7 Limitations and Future Work
A Appendix
A.1 Slicing Algorithm and Illustration
References
Formal Methods for Software Engineering
Structuring Formal Methods into the Undergraduate Computer Science Curriculum
1 Introduction
2 The Current Situation
2.1 Developing Coursework and Pedagogy
2.2 The Mathematics Connection in Computer Science Program
2.3 Pedagogical Challenges and Approaches
2.4 Experiences and Observations
3 Possible Initiatives (Recommendations)
3.1 A Framework for the Undergraduate Curriculum
3.2 Special Recognition for Higher Standards
3.3 Exerting Influence Through Prominent Bodies
4 Conclusions
References
Integrated Contract-Based Unit and System Testing for Component-Based Systems
1 Introduction
2 Background
3 System Testing Framework Overview
4 Example
5 System Test Scripting Framework
5.1 Observations and Injections
5.2 Properties
5.3 Controlled Trace Exploration
5.4 Test Run Configuration
6 Auto-generated Test Reports
7 Experience Report
8 Related Work
9 Conclusion
References
Verifying PLC Programs via Monitors: Extending the Integration of FRET and PLCverif
1 Introduction
2 Preliminaries: PLC Verification and Specification
3 Generating Monitors for PLTL Properties
4 Case Study
5 Conclusion
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken