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(Editor)

Springer (Publisher)

Published on 6. April 2018

XI, 470 pages

E-Book

PDF with digital watermarking

System requirements

978-3-319-77935-5 (ISBN)

€53.49incl. 7% vat

System requirements

for PDF with digital watermarking

E-Book Single Licence

Available for download

Description

More details

Other editions

Content

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

System requirements

Save as PDF Copy link into clipboard

Schweitzer Fachinformationen

NASA Formal Methods

Description

More details

Other editions

Additional editions

Content

System requirements