NASA Formal Methods

✍ Scribed by Clark Barrett and Misty Davies

• Publisher: Springer
• Year: 2017
• Tongue: English
• Leaves: 448
• Category: Library

✦ Synopsis

This book constitutes the proceedings of the 9th International Symposium on NASA Formal Methods, NFM 2017, held in Moffett Field, CA, USA, in May 2017.

The 23 full and 8 short papers presented in this volume were carefully reviewed and selected from 77 submissions. The papers focus on formal techniques and other approaches for software assurance, their theory, current capabilities and limitations, as well as their potential application to aerospace, robotics, and other NASA-relevant safety-critical systems during all stages of the software life-cycle.

✦ Table of Contents

Front Matter....Pages I-XI
An Automata-Theoretic Approach to Modeling Systems and Specifications over Infinite Data....Pages 1-18
Learning from Faults: Mutation Testing in Active Automata Learning....Pages 19-34
Parametric Model Checking Timed Automata Under Non-Zenoness Assumption....Pages 35-51
Multi-timed Bisimulation for Distributed Timed Automata....Pages 52-67
Auto-Active Proof of Red-Black Trees in SPARK....Pages 68-83
Analysing Security Protocols Using Refinement in iUML-B....Pages 84-98
On Learning Sparse Boolean Formulae for Explaining AI Decisions....Pages 99-114
Event-Based Runtime Verification of Temporal Properties Using Time Basic Petri Nets....Pages 115-130
Model-Counting Approaches for Nonlinear Numerical Constraints....Pages 131-138
Input Space Partitioning to Enable Massively Parallel Proof....Pages 139-145
Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations....Pages 146-162
Modular Model-Checking of a Byzantine Fault-Tolerant Protocol....Pages 163-177
Improved Learning for Stochastic Timed Models by State-Merging Algorithms....Pages 178-193
Verifying Safety and Persistence Properties of Hybrid Systems Using Flowpipes and Continuous Invariants....Pages 194-211
A Relational Shape Abstract Domain....Pages 212-229
Floating-Point Format Inference in Mixed-Precision....Pages 230-246
A Verification Technique for Deterministic Parallel Programs....Pages 247-264
Systematic Predicate Abstraction Using Variable Roles....Pages 265-281
HyPro: A C++ Library of State Set Representations for Hybrid Systems Reachability Analysis....Pages 282-287
SPEN: A Solver for Separation Logic....Pages 288-294
From Hazard Analysis to Hazard Mitigation Planning: The Automated Driving Case....Pages 295-301
Event-B at Work: Some Lessons Learnt from an Application to a Robot Anti-collision Function....Pages 302-309
Reasoning About Safety-Critical Information Flow Between Pilot and Computer....Pages 310-326
Compositional Falsification of Cyber-Physical Systems with Machine Learning Components....Pages 327-341
Verifying a Class of Certifying Distributed Programs....Pages 342-356
Compact Proof Witnesses....Pages 357-372
Qualification of a Model Checker for Avionics Software Verification....Pages 373-388
SpeAR v2.0: Formalized Past LTL Specification and Analysis of Requirements....Pages 389-403
Just Formal Enough? Automated Analysis of EARS Requirements....Pages 404-419
Back Matter....Pages 420-426
....Pages 427-434