NASA Formal Methods

Name: NASA Formal Methods | 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings

Clark Barrett Misty Davies Temesghen Kahsai(Herausgeber*in)

Springer (Verlag)

Erschienen am 8. April 2017

XI, 436 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-57288-8 (ISBN)

53,49 €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
Contents
An Automata-Theoretic Approach to Modeling Systems and Specifications over Infinite Data
1 Introduction
2 Preliminaries
3 Variable Automata: Non-determinism Vs. Alternation
3.1 NVBWs Are Not Expressive Enough for *-VLTL
3.2 Alternating Variable Büchi Automata
3.3 AVBWs Can Express All of *-VLTL
3.4 AVBWs Are Not Complementable
3.5 Variable Automata: From AVBW to NVBW
4 Fragments of *-VLTL Expressible by NVBWs
5 Model Checking in Practice
6 Conclusions and Future Work
References
Learning from Faults: Mutation Testing in Active Automata Learning
1 Introduction
2 Related Work
3 Preliminaries
3.1 Mealy Machines
3.2 Active Automata Learning
4 Test-Suite Generation
4.1 Test-Case Generation
4.2 Test-Case Selection
4.3 Mutation-Based Selection
5 Evaluation
5.1 Measurement Setup
6 Conclusion
References
Parametric Model Checking Timed Automata Under Non-Zenoness Assumption
1 Introduction
2 Preliminaries
3 Undecidability of the Non-Zeno Emptiness Problem
4 CUB-Parametric Timed Automata
4.1 Parametric Clock Upper Bounds
4.2 CUB Parametric Timed Automata
4.3 CUB PTA Detection
4.4 Transforming a PTA into a Disjunctive CUB-PTA
5 Zeno-Free Cycle Synthesis in CUB-PTAs
6 Experiments
7 Conclusion
References
Multi-timed Bisimulation for Distributed Timed Automata
1 Introduction
2 Preliminaries
3 An Alternative Semantics for DTA
3.1 Multi-timed Actions
3.2 Multi-timed Labeled Transition Systems
3.3 A Multi-timed Semantics for icTA
4 Multi-timed Bisimulation
4.1 Strong Multi-timed Bisimulation
4.2 Decidability
5 Related Work
6 Conclusions
References
Auto-Active Proof of Red-Black Trees in SPARK
1 Introduction
2 Preliminaries
2.1 SPARK 2014
2.2 Auto-Active Verification
2.3 Red-Black Trees
3 Red-Black Trees in SPARK
3.1 Invariants and Models
3.2 Implementation
3.3 Specification
3.4 Proof Principles
3.5 Ghost Code
4 Development and Verification Data
5 Related Work
6 Conclusion
References
Analysing Security Protocols Using Refinement in iUML-B
1 Introduction
2 Background
2.1 VLAN Tagging
2.2 Event-B
2.3 iUML-B
2.4 Validation and Verification
3 Development
3.1 M0: An Abstract Model of VLAN Security
3.2 M1: Introducing Switches and Devices
3.3 M2: Introducing Tagging
3.4 Analysis
4 Summary of Approach
5 Conclusion
References
On Learning Sparse Boolean Formulae for Explaining AI Decisions
1 Introduction
2 Motivating Example
3 Problem Definition
4 Learning Explanations as Sparse Boolean Formula
5 Experiments
6 Related Work
7 Conclusion and Future Work
References
Event-Based Runtime Verification of Temporal Properties Using Time Basic Petri Nets
1 Introduction
2 Background on Time Basic Nets
3 Event-Based Runtime Verification
4 The MahaRAJA Framework
5 Experimental Validation
6 Related Work and Comparative Evaluation
7 Conclusion
References
Model-Counting Approaches for Nonlinear Numerical Constraints
1 Introduction
1.1 Symbolic Execution and SPF
1.2 Quantification of Information Leaks
2 Model Counting Techniques and Tools
3 Evaluation
4 Conclusion
References
Input Space Partitioning to Enable Massively Parallel Proof
1 Introduction
2 Input Space Partitioning and Parallel Proof
3 Reducing Per-Slice Proof Time
4 Case Study
5 Conclusion
References
Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations
1 Introduction
2 The New Danish Route-Based Interlocking Systems
2.1 Specification of Interlocking Systems
2.2 The RobustRailS Verification Method and Toolkit
3 Method
3.1 Linear Cuts on Multiple Station Lines
3.2 A Compositional Model Checking Approach
4 Soundness and Completeness of the Approach
4.1 Soundness
4.2 Completeness
5 Experiments
5.1 Experimental Approach
5.2 Two Stations Case Study
5.3 EDL: The Real World Case Study
6 Conclusion
References
Modular Model-Checking of a Byzantine Fault-Tolerant Protocol
1 Introduction
2 Formal Model
2.1 Calendar Automata
2.2 Symbolic Fault Injection: A Synchronous Kibitzer
2.3 Abstract Transition Systems
3 Modeling and Verification for Oral Messages
3.1 OMH (m) Algorithm
3.2 Model Sketch
3.3 Invariants
4 Experimental Results
4.1 Scalability
4.2 Modular Verification
4.3 Proof Effort Remarks
5 Related Work
6 Conclusions
References
Improved Learning for Stochastic Timed Models by State-Merging Algorithms
1 Introduction
2 Related Works
3 Background
3.1 Deterministic Real-Time Automata (DRTA)
3.2 Stochastic Interpretation of a DRTA
4 The RTI+ Learning Procedure
4.1 Building the APTA
4.2 The Learning Process
4.3 Compatibility Evaluation
4.4 Shortcomings
5 Learning More Accurate Models
5.1 Unfolded APTA
5.2 Constructive-Bound APTA
5.3 Tightened-Bound APTA
5.4 Evaluation
6 Experiments
6.1 Evaluation Procedure
6.2 Benchmarks
6.3 Results
7 Conclusion
References
Verifying Safety and Persistence Properties of Hybrid Systems Using Flowpipes and Continuous Invariants
1 Introduction
2 Safety and Persistence for Hybrid Automata
2.1 Preliminaries
2.2 Bounded Time Safety and Eventuality
2.3 Unbounded Time Safety
2.4 Combining Unbounded Time Safety with Eventuality to Prove Persistence
2.5 Using Persistence to Prove Safety
3 An Example Persistence Verification Problem
4 Verifying Persistence
4.1 Continuous Invariant
4.2 Verified Integration
5 Outlook and Challenges to Automation
6 Related Work
7 Conclusion
References
A Relational Shape Abstract Domain
1 Introduction
2 Overview and Motivating Example
3 Concrete Semantics
4 Abstraction
5 Analysis Algorithms
5.1 Basic Abstract Post-conditions
5.2 Materialization and General Abstract Post-conditions
5.3 Folding and Lattice Operations
5.4 Analysis
6 Experimental Evaluation
7 Related Works
8 Conclusion
References
Floating-Point Format Inference in Mixed-Precision
1 Introduction
2 Preliminary Elements
2.1 Elements of Floating-Point Arithmetic
2.2 Overview of Our Method
2.3 Related Work
3 Abstract Semantics
3.1 Abstract Domain
3.2 Transfer Functions
4 Constraint Generation
4.1 Constraints for Arithmetic Expressions
4.2 Systematic Constraint Generation
5 Experimental Results
6 Conclusion
References
A Verification Technique for Deterministic Parallel Programs
1 Introduction
2 Background
2.1 OpenMP
2.2 Permission-Based Separation Logic
2.3 Iteration Contract
3 Syntax and Semantics of Deterministic Parallelism
3.1 Syntax
3.2 Semantics
4 Verification Approach
4.1 Verification
4.2 Soundness
5 Verification of OpenMP Programs
6 Related Work
7 Conclusion and Future Work
References
Systematic Predicate Abstraction Using Variable Roles
1 Introduction
1.1 Introductory Examples of Domain-Specific Abstraction
2 Predicate Abstraction and Refinement
2.1 Solving Horn Clauses with Predicate Abstraction
2.2 Craig Interpolation with Templates
3 Role-Based Predicates and Templates
3.1 Definition of Roles
3.2 Role-Based Predicates and Templates
4 Evaluation
References
specgen: A Tool for Modeling Statecharts in CSP
1 Introduction
2 The Dining Philosophers: An Example
2.1 The Generated Model
2.2 Finding the Deadlock
2.3 More Complicated Properties
2.4 Performance
3 Translation Enhancements
4 Conclusion and Future Work
References
HYPRO: A C++ Library of State Set Representations for Hybrid Systems Reachability Analysis
1 Introduction
2 Hybrid Systems Reachability Analysis
3 The HYPRO Library
4 Experimental Evaluation
References
Asm2C++: A Tool for Code Generation from Abstract State Machines to Arduino
1 Introduction
2 Abstract State Machine Methodology
3 Code Generation Process
4 Illustrative Example
5 Related Work
6 Conclusions and Future Work
References
SPEN: A Solver for Separation Logic
1 Introduction
2 Logic Fragment
3 Satisfiability Checking
4 Entailment Checking
5 Experimental Results
References
From Hazard Analysis to Hazard Mitigation Planning: The Automated Driving Case
1 Challenges, Background, and Contribution
2 Related Work
3 Abstraction for Run-Time Hazard Mitigation
4 Concepts for Run-Time Hazard Mitigation
5 Construction of Risk Structures
6 Example: Fail-Operational Driver Assistance
7 Discussion of Limitations, Applicability, and Strengths
8 Conclusion and Future Work
References
Event-B at Work: Some Lessons Learnt from an Application to a Robot Anti-collision Function
Abstract
1 Introduction
2 Formal Refinement in an Industrial Development Process
3 The Case Study
3.1 The TwIRTee Rover and the ARP Function
3.2 Rodin and Event-B
4 From System-Level Requirements to High-Level Requirements
4.1 Building a Refinement Strategy
4.2 Formalization of Requirements
4.3 Verification of Refinements
4.4 Validation of Formal Requirements
4.5 Model Review
5 Related Works
6 Conclusion
References
Reasoning About Safety-Critical Information Flow Between Pilot and Computer
1 Introduction
2 Dynamic Agent Safety Logic
2.1 Syntax and Semantics
2.2 Hilbert System
2.3 Soundness
3 Case Study and Mechanization
3.1 Air France 447
3.2 Mechanization in Coq
4 Future Work
5 Conclusion
References
Compositional Falsification of Cyber-Physical Systems with Machine Learning Components
1 Introduction
2 Background
2.1 CPSML Models
2.2 Signal Temporal Logic
3 Compositional Falsification Framework
4 Machine Learning Analyzer
4.1 Feature Space Abstraction
4.2 Approximation of Learning Components
5 Experimental Results
5.1 Implementation Details
5.2 Case Studies
6 Conclusion
References
Verifying a Class of Certifying Distributed Programs
1 Introduction
1.1 Structure of this Paper
2 Preliminaries
2.1 Certifying Sequential Programs
2.2 Verification of Certifying Sequential Programs
3 Verification Method for a Class of Certifying Distributed Programs
3.1 Distributed Programs
3.2 Challenges of Certifying Distributed Programs
3.3 A Class of Certifying Distributed Programs
3.4 Verification Method for Class C
3.5 Further Classes of Certifying Distributed Programs
4 Case Study: Leader Election
4.1 Certifying Leader Election
4.2 Verification in Coq
5 Related Work
6 Conclusion
7 Future Work
References
Compact Proof Witnesses
1 Introduction
2 Background
3 Proof Witnesses and Weakenings
4 Variable-Separate Analyses
5 Experiments
6 Conclusion
References
Qualification of a Model Checker for Avionics Software Verification
1 Introduction
2 Aircraft Software and Certification
3 Qualification
3.1 Tool Qualification Level
3.2 DO-330 and Tool Qualification Objectives
4 Case Study: Kind 2 Model Checker
4.1 Need for Tool Qualification
4.2 Tool Qualification Objectives
4.3 Results
5 Case Study: Proof-Generating Model Checker
5.1 Development of a Proof-Generating Version of Kind 2
5.2 Qualification of Check-It
5.3 Results
6 Conclusions
References
SpeAR v2.0: Formalized Past LTL Specification and Analysis of Requirements
1 Introduction
2 Related Work
3 Formal Requirements Capture
3.1 SpeAR File Stucture
3.2 SpeAR Formal Semantics
4 Analysis
4.1 Logical Entailment
4.2 Logical Consistency
5 Conclusion and Future Work
References
Just Formal Enough? Automated Analysis of EARS Requirements
1 Introduction
2 Running Example
3 Expressing and Analyzing Requirements
3.1 Well-Formedness by Construction
3.2 Realizability Analysis
3.3 The EARS-CTRL Tool
4 Related Work
5 Conclusions and Future Work
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken