NASA Formal Methods

Name: NASA Formal Methods | 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings

Aaron Dutle César Muñoz Anthony Narkawicz(Herausgeber*in)

Springer (Verlag)

Erschienen am 6. April 2018

XI, 470 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-77935-5 (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
Incremental Construction of Realizable Choreographies
1 Introduction
2 Background and Notations
2.1 Model
2.2 Realizability
3 CCP Language for Realisable CPs
3.1 Composition Operators
3.2 Realizable-by-Construction CP
4 CCP Model: Refinement-Based Realizability
4.1 The Refinement Strategy
4.2 The Root Model
4.3 First Refinement: Synchronous Model
4.4 Second Refinement: Asynchronous Model
4.5 Instantiation and Axiom Validation
4.6 Assessment
5 Related Work
6 Conclusion
References
Formal Assurance for Cooperative Intelligent Autonomous Agents
1 Introduction
2 Related Work
3 Modeling and Formal Verification
3.1 Cognitive Architectures and Frameworks: Soar
3.2 Formal Languages and Verification: Uppaal
4 Example Case Study: Engine Out Contingency During Takeoff
5 Automated Translation from Cognitive Architecture to Formal Environment
5.1 Automated Translation to Uppaal
5.2 Translation Implementation
6 Verification and Validation Efforts
6.1 Simulation Efforts for Validation of the Autonomous Pilot Agent
6.2 Formal Verification of the Autonomous Pilot Agent
7 Conclusion and Future Work
References
Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C
1 Introduction
2 The List Module of Contiki
3 The Verification Approach
3.1 Running Example
3.2 List Representation by a Companion Ghost Array
3.3 Formal Specification
3.4 Ghost Functions
3.5 Auxiliary Lemmas and Proofs
3.6 Results of the Verification
3.7 Validation of Specification
4 Related Work
5 Conclusion and Future Work
References
An Executable Formal Framework for Safety-Critical Human Multitasking
1 Introduction
2 Preliminaries
3 A Formal Model of Human Multitasking
3.1 Classes
3.2 Dynamic Behavior
4 Analyzing Safety-Critical Human Multitasking
5 Example: Interacting with a GPS Device While Driving
6 Related Work
7 Concluding Remarks
References
Simpler Specifications and Easier Proofs of Distributed Algorithms Using History Variables
1 Introduction
2 Specifications Using Message History Variables
3 Invariants and Proofs Using Message History Variables
4 Multi-Paxos
5 Results
6 Related Work and Conclusion
References
Don't Miss the End: Preventing Unsafe End-of-File Comparisons
1 Introduction
2 Type System
2.1 Type Qualifiers and Qualifier Hierarchy
2.2 Type Casting Rules
2.3 Default Qualifiers
2.4 Data-Flow-Sensitive Type Refinement
3 Implementation
4 Experiments
5 Related Work
6 Conclusions
References
An Efficient Rewriting Framework for Trace Coverage of Symmetric Systems
1 Introduction
2 Related Work
3 Preliminaries
4 Strategy Overview
4.1 Rewriting Systems
4.2 Abstraction and Coverage Model
5 Conservative Abstraction
5.1 Abstractable Composed-Systems
5.2 Trace Abstraction
5.3 Abstract Trace Rewriting
5.4 Coverage Holes
6 Experiments
6.1 The MIST Protocol
6.2 Model Viability
6.3 Effectiveness
6.4 Monitor-Centric Experiments
6.5 Experiments on a Large-Scale Verification Environment
7 Conclusion
References
Verification of Fault-Tolerant Protocols with Sally
1 Introduction
2 Sally
3 Modeling Fault-Tolerant Protocols
3.1 Approximate Agreement
3.2 Verification Results
4 Related Work
5 Conclusion
References
Output Range Analysis for Deep Feedforward Neural Networks
1 Introduction
2 Preliminaries
2.1 Mixed Integer Linear Programs
3 Problem Definition and MILP Encoding
3.1 MILP Encoding
4 Combining MILP Solvers with Local Search
4.1 Overall Approach
4.2 Local Search Improvement
5 Application: Reachability Analysis
6 Experimental Evaluation
7 Conclusion
References
Formal Dynamic Fault Trees Analysis Using an Integration of Theorem Proving and Model Checking
1 Introduction
2 Related Work
3 Proposed Methodology
4 Formalization of Dynamic Fault Trees in HOL
4.1 Identity Elements
4.2 Temporal Operators
4.3 Fault Tree Gates
4.4 Formal Verification of the Simplification Theorems
5 Experimental Results
5.1 Formal Verification of the Reduced Cascaded PAND DFT
5.2 Quantitative Analysis Results Using STORM
6 Conclusion
References
Twenty Percent and a Few Days - Optimising a Bitcoin Majority Attack
1 Introduction
2 The Bitcoin Protocol
3 Model and Strategies
4 Analysis
5 Conclusion
References
An Even Better Approach - Improving the B.A.T.M.A.N. Protocol Through Formal Modelling and Analysis
1 Introduction
2 The B.A.T.M.A.N. Protocol
2.1 Literal Model
2.2 Alternative Model
3 Uppaal Model
4 Simulation Results
5 Conclusion
References
Towards a Formal Safety Framework for Trajectories
1 Introduction
2 The Framework
3 Trajectory Validation Strategy
4 Conclusion and Future Work
References
Static Value Analysis of Python Programs by Abstract Interpretation
1 Introduction
2 The Mini-Python Language
2.1 Syntax
2.2 Concrete Collecting Semantics
3 Value Abstraction
3.1 Non-relational Abstraction
3.2 Relational Abstraction
4 Generator Analysis
4.1 Concrete Semantics
4.2 Abstractions
5 Experimental Evaluation
6 Related Work
7 Conclusion
References
Model-Based Testing for General Stochastic Time
1 Introduction
2 Background
3 Stochastic Testing Theory
3.1 Test Cases
3.2 Stochastic Input-Output Conformance and Annotations
3.3 Test Execution and Sampling
3.4 Test Evaluation and Correctness
4 Implementing Stochastic Testing
4.1 Goodness of Fit
4.2 Algorithm Outline
5 Experiments
6 Conclusion
References
Strategy Synthesis for Autonomous Agents Using PRISM
1 Introduction
2 Background
3 Scenarios
4 Conclusions and Future Work
References
The Use of Automated Theory Formation in Support of Hazard Analysis
1 Introduction
2 Background
3 Experiments with a Simple Design Model
3.1 Applying HR to the Laser Control System
3.2 Discovering Properties in Support of Hazard Analysis
3.3 Breaking Properties
4 Future Work and Conclusion
References
Distributed Model Checking Using ProB
1 Introduction
1.1 B and ProB
2 Architecture Overview
3 Implementation
3.1 Socket Patterns and Messages
3.2 When is a Model Suitable for Distributed Model Checking?
3.3 Passing States to C
3.4 Visited States
3.5 Work Sharing
3.6 Proxy
3.7 Bandwidth Reduction
4 Evaluation
5 Related Work
6 Conclusion and Future Work
References
Optimal Storage of Combinatorial State Spaces
1 Introduction
2 An Information Theoretical Lower Bound
3 An Analysis of Binary Tree Compression
4 A Novel Compact Tree
5 Experiments
6 Discussion and Conclusion
References
Stubborn Transaction Reduction
1 Introduction
2 Preliminaries
3 Stubborn Transaction Reduction
3.1 Parametrized Stubborn Sets
3.2 Reduced Transaction Systems
4 Comparison Between TR and POR
5 Experiments
6 Related Work
7 Conclusion
References
Certified Foata Normalization for Generalized Traces
1 Introduction
2 Traces, Foata Normal Forms and Normalization
3 Formalization
3.1 Traces
3.2 Normal Forms
3.3 Normalization
3.4 Properties
4 Example: Local Reads in TSO
5 Related Work
6 Conclusion and Future Work
References
On the Timed Analysis of Big-Data Applications
1 Introduction
2 Background
2.1 Apache Spark Framework
2.2 Constraint LTL over-clocks
3 Modeling Spark Applications
4 Implementation and Validation of the Model
5 Related Works
6 Conclusion
References
Tuning Permissiveness of Active Safety Monitors for Autonomous Systems
1 Introduction
2 Related Work
3 Baseline and Concepts
3.1 Safety Invariants, Margins and States
3.2 Safety and Permissiveness Properties
3.3 SMOF Tooling
3.4 On Tuning Permissiveness Properties
4 Defining Custom Permissiveness Properties
4.1 A Formal Model for the Permissiveness
4.2 Binding Together Invariants and Permissiveness
4.3 Restricting Functionalities
4.4 Integration in SMOF Tooling
5 Application to an Example
5.1 SI1: The Arm Must Not Be Extended when the Platform Moves over a Certain Speed
5.2 SI2: A Gripped Box Must Not Be Tilted More Than 0
5.3 SI3: The Robot Must Not Enter a Prohibited Zone
6 Conclusion and Perspectives
References
Sound Black-Box Checking in the LearnLib
1 Introduction
2 Preliminaries
2.1 LTL Model Checking
2.2 Active Learning
2.3 Black-Box Checking
3 Sound Black-Box Checking
3.1 Validating Lassos with State Equivalence
3.2 Implementation in the LearnLib
4 Related Work
5 Results
6 Conclusion
References
Model-Checking Task Parallel Programs for Data-Race
1 Introduction
2 Example
3 Task Parallel Programs
3.1 Computation Graphs
3.2 Programming Model
4 Proof of Correctness
5 Implementation and Results
6 Related Work
7 Conclusion and Future Work
References
Consistency of Property Specification Patterns with Boolean and Constrained Numerical Signals
1 Introduction
2 Background and Related Work
3 Constraint Property Specification Patterns
4 Analysis with Probabilistic Requirement Generation
5 Analysis with a Controller for a Robotic Manipulator
6 Conclusions
References
Automatic Generation of DO-178 Test Procedures
1 Introduction
2 Industrial Context
2.1 Running HLR Example
2.2 Software Test Standards
2.3 Running Example: TCs for Req1
2.4 Running Example: TP Implementation for Req1
3 Liebherr Test Specification Language
3.1 Syntax
3.2 Semantics
3.3 Running Example: Req1 TCs Expressed in LTSL
4 SCADE Observers Generation
4.1 SCADE Automata Syntax
4.2 Translation Function
5 Illustration of the Approach
6 Related Work
7 Conclusion
References
Using Test Ranges to Improve Symbolic Execution
1 Introduction
2 The SynergiSE Approach
2.1 Traditional Ranges
2.2 SynergiSE with Feasible Range
2.3 SynergiSE with Unexplored Range
3 Evaluation
3.1 Implementation and Subjects
3.2 SynergiSE with Feasible Ranges
3.3 SynergiSE for Integrating Test Generation Tools
3.4 SynergiSE for Sharing Constraint Solving Results Among Workers
4 Related Work
5 Conclusion
References
Symbolic Execution and Reachability Analysis Using Rewriting Modulo SMT for Spatial Concurrent Constraint Systems with Extrusion
1 Introduction
2 Preliminaries
3 Spatial Concurrent Constraint Systems with Extrusion
4 Symbolic Rewriting Logic Semantics
4.1 The Constraint System
4.2 System States
4.3 System Transitions
4.4 Admissibility
5 Symbolic Reachability Analysis
5.1 Fault-Tolerance and Consistency
5.2 Knowledge Inference
5.3 Same Knowledge
6 Related Work and Concluding Remarks
References
Experience Report: Application of Falsification Methods on the UxAS System
1 Introduction
2 Problem Statement
3 Test Generation for UxAS
3.1 Case-Study
4 Conclusion and Future Work
References
MoDeS3: Model-Based Demonstrator for Smart and Safe Cyber-Physical Systems
1 Introduction
2 Design- and Runtime Assurance
2.1 Design-Time Formal V&V of Timing Properties
2.2 System-Level Runtime Monitoring
3 Smart IoT Technologies
4 MoDeS3 in Education
5 Project Timeline and Conclusion
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken