NASA Formal Methods: 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings (Lecture Notes in Computer Science Book 9690)

This book constitutes the proceedings of the 8th International Symposium on NASA Formal Methods, NFM 2016, held in Minneapolis, MN, USA, in June 2016. The 19 full and 10 short papers presented in this volume were carefully reviewed and selected from 70 submissions. The papers were organized in topical sections named: requirements and architectures; testing and run-time enforcement; theorem proving and proofs; application of formal methods; code generation and synthesis; model checking and verification; and correctness and certification. Front Matter....Pages I-XIX Front Matter....Pages 1-1 Temporal Logic Framework for Performance Analysis of Architectures of Systems....Pages 3-18 On Implementing Real-Time Specification Patterns Using Observers....Pages 19-33 Contract-Based Verification of Complex Time-Dependent Behaviors in Avionic Systems....Pages 34-40 ARSENAL: Automatic Requirements Specification Extraction from Natural Language....Pages 41-46 Front Matter....Pages 47-47 Assisted Coverage Closure....Pages 49-64 Synthesizing Runtime Enforcer of Safety Properties Under Burst Error....Pages 65-81 Compositional Runtime Enforcement....Pages 82-99 Improving an Industrial Test Generation Tool Using SMT Solver....Pages 100-106 The comKorat Tool: Unified Combinatorial and Constraint-Based Generation of Structurally Complex Tests....Pages 107-113 Front Matter....Pages 115-115 Automated Synthesis of Safe Autonomous Vehicle Control Under Perception Uncertainty....Pages 117-132 Obfuscator Synthesis for Privacy and Utility....Pages 133-149 Code Generation Using a Formal Model of Reference Counting....Pages 150-165 EventB2Java: A Code Generator for Event-B....Pages 166-171 Front Matter....Pages 173-173 A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles....Pages 175-190 Probabilistic Formal Verification of the SATS Concept of Operation....Pages 191-205 Formal Translation of IEC 61131-3 Function Block Diagrams to PVS with Nuclear Application....Pages 206-220 Formal Analysis of Extended Well-Clear Boundaries for Unmanned Aircraft....Pages 221-226 Formal Validation and Verification Framework for Model-Based and Adaptive Control Systems....Pages 227-233 Front Matter....Pages 235-235 Verifying Relative Safety, Accuracy, and Termination for Program Approximations....Pages 237-254 Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis....Pages 255-271 Front Matter....Pages 235-235 Gray-Box Learning of Serial Compositions of Mealy Machines....Pages 272-287 Front Matter....Pages 289-289 Specification and Proof of High-Level Functional Properties of Bit-Level Programs....Pages 291-306 Formal Verification of an Executable LTL Model Checker with Partial Order Reduction....Pages 307-321 A Modular Way to Reason About Iteration....Pages 322-336 A Proof Infrastructure for Binary Programs....Pages 337-343 Hierarchical Verification of Quantum Circuits....Pages 344-352 Front Matter....Pages 353-353 Semantics for Locking Specifications....Pages 355-372 From Design Contracts to Component Requirements Verification....Pages 373-387 A Hybrid Architecture for Correct-by-Construction Hybrid Planning and Control....Pages 388-394 Back Matter....Pages 395-396