NASA Formal Methods: 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings (Lecture Notes in Computer Science Book 10227)

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. 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 This volume contains the papers presented at ATVA 2007,the 5th International Symposium on Automated Technology for Veri?cation and Analysis, which was held onOctober22-25,2007atthe NationalCenter ofSciencesin Tokyo, Japan. The purpose of ATVA is to promote research on theoretical and practical aspects of automated analysis, veri?cationand synthesis in East Asia by prov- ing a forum for interaction between the regional and the international research communities and industry in the?eld. The?rst three ATVA symposia were held in 2003, 2004 and 2005 in Taipei, and ATVA 2006 was held in Beijing. Theprogramwasselectedfrom88submitted papers, with25countriesrep- sented among the authors. Of these submissions, 29 regular papers and 7 short papers were selected for inclusion in the program. In addition, the program included keynote talks and tutorials by Martin Abadi (University of California, Santa Cruz and Microsoft Research), Ken McMillan (Cadence Berkeley Labs), and Moshe Vardi (Rice University), and an invited talk by Atsushi Hasegawa (Renesas Technology). A workshop on Omega-Automata (OMEGA 2007) was organized in connection with the conference. ATVA 2007 was sponsored by the National Institute of Informatics, the Kayamori Foundation of Information Science Advancement, the Inoue Fo- dation for Science, and the Telecommunications Advancement Foundation. We are grateful for their support. We would like to thank the program committee and the reviewers for their hard work and dedication in putting together this program. We would like to thank the Steering Committee for their considerable help with the organization of the conference. We also thank Michihiro Koibuchi for his help with the local arrangements This book constitutes the refereed proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis, ATVA 2007, held in Tokyo, Japan, October 22-25, 2007. The 29 revised full papers presented together with 7 short papers were carefully reviewed and selected from 88 submissions. The papers address theoretical methods to achieve correct software or hardware systems, including both functional and non functional aspects; as well as applications of theory in engineering methods and particular domains and handling of practical problems occurring in tools This book constitutes the refereed proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis, ATVA 2007. The 29 revised full papers presented together with seven short papers address theoretical methods to achieve correct software or hardware systems, including both functional and non functional aspects; as well as applications of theory in engineering methods and particular domains and handling of practical problems occurring in tools.