Nasa Formal Methods: 10th International Symposium, Nfm 2018, Newport News, Va, Usa, April 17-19, 2018, Proceedings (lecture Notes In Computer Science)

This book constitutes the proceedings of the 10th International Symposium on NASA Formal Methods, NFM 2018, held in Newport News, VA, USA, in April 2018 . The 24 full and 7 short papers presented in this volume were carefully reviewed and selected from 92 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 Incremental Construction of Realizable Choreographies (Sarah Benyagoub, Meriem Ouederni, Yamine Aït-Ameur, Atif Mashkoor)....Pages 1-19 Formal Assurance for Cooperative Intelligent Autonomous Agents (Siddhartha Bhattacharyya, Thomas C. Eskridge, Natasha A. Neogi, Marco Carvalho, Milton Stafford)....Pages 20-36 Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C (Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue)....Pages 37-53 An Executable Formal Framework for Safety-Critical Human Multitasking (Giovanna Broccia, Paolo Milazzo, Peter Csaba Ölveczky)....Pages 54-69 Simpler Specifications and Easier Proofs of Distributed Algorithms Using History Variables (Saksham Chand, Yanhong A. Liu)....Pages 70-86 Don’t Miss the End: Preventing Unsafe End-of-File Comparisons (Charles Zhuo Chen, Werner Dietl)....Pages 87-94 An Efficient Rewriting Framework for Trace Coverage of Symmetric Systems (Flavio M. De Paula, Arvind Haran, Brad Bingham)....Pages 95-112 Verification of Fault-Tolerant Protocols with Sally (Bruno Dutertre, Dejan Jovanović, Jorge A. Navas)....Pages 113-120 Output Range Analysis for Deep Feedforward Neural Networks (Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, Ashish Tiwari)....Pages 121-138 Formal Dynamic Fault Trees Analysis Using an Integration of Theorem Proving and Model Checking (Yassmeen Elderhalli, Osman Hasan, Waqar Ahmad, Sofiène Tahar)....Pages 139-156 Twenty Percent and a Few Days – Optimising a Bitcoin Majority Attack (Ansgar Fehnker, Kaylash Chaudhary)....Pages 157-163 An Even Better Approach – Improving the B.A.T.M.A.N. Protocol Through Formal Modelling and Analysis (Ansgar Fehnker, Kaylash Chaudhary, Vinay Mehta)....Pages 164-178 Towards a Formal Safety Framework for Trajectories (Marco A. Feliú, Mariano M. Moscato)....Pages 179-184 Static Value Analysis of Python Programs by Abstract Interpretation (Aymeric Fromherz, Abdelraouf Ouadjaout, Antoine Miné)....Pages 185-202 Model-Based Testing for General Stochastic Time (Marcus Gerhold, Arnd Hartmanns, Mariëlle Stoelinga)....Pages 203-219 Strategy Synthesis for Autonomous Agents Using PRISM (Ruben Giaquinta, Ruth Hoffmann, Murray Ireland, Alice Miller, Gethin Norman)....Pages 220-236 The Use of Automated Theory Formation in Support of Hazard Analysis (Andrew Ireland, Maria Teresa Llano, Simon Colton)....Pages 237-243 Distributed Model Checking Using ProB (Philipp Körner, Jens Bendisposto)....Pages 244-260 Optimal Storage of Combinatorial State Spaces (Alfons Laarman)....Pages 261-279 Stubborn Transaction Reduction (Alfons Laarman)....Pages 280-298 Certified Foata Normalization for Generalized Traces (Hendrik Maarand, Tarmo Uustalu)....Pages 299-314 On the Timed Analysis of Big-Data Applications (Francesco Marconi, Giovanni Quattrocchi, Luciano Baresi, Marcello M. Bersani, Matteo Rossi)....Pages 315-332 Tuning Permissiveness of Active Safety Monitors for Autonomous Systems (Lola Masson, Jérémie Guiochet, Hélène Waeselynck, Kalou Cabrera, Sofia Cassel, Martin Törngren)....Pages 333-348 Sound Black-Box Checking in the LearnLib (Jeroen Meijer, Jaco van de Pol)....Pages 349-366 Model-Checking Task Parallel Programs for Data-Race (Radha Nakade, Eric Mercer, Peter Aldous, Jay McCarthy)....Pages 367-382 Consistency of Property Specification Patterns with Boolean and Constrained Numerical Signals (Massimo Narizzano, Luca Pulina, Armando Tacchella, Simone Vuotto)....Pages 383-398 Automatic Generation of DO-178 Test Procedures (César Ochoa Escudero, Rémi Delmas, Thomas Bochot, Matthieu David, Virginie Wiels)....Pages 399-415 Using Test Ranges to Improve Symbolic Execution (Rui Qiu, Sarfraz Khurshid, Corina S. Păsăreanu, Junye Wen, Guowei Yang)....Pages 416-434 Symbolic Execution and Reachability Analysis Using Rewriting Modulo SMT for Spatial Concurrent Constraint Systems with Extrusion (Miguel Romero, Camilo Rocha)....Pages 435-451 Experience Report: Application of Falsification Methods on the UxAS System (Cumhur Erkan Tuncali, Bardh Hoxha, Guohui Ding, Georgios Fainekos, Sriram Sankaranarayanan)....Pages 452-459 MoDeS3: Model-Based Demonstrator for Smart and Safe Cyber-Physical Systems (András Vörös, Márton Búr, István Ráth, Ákos Horváth, Zoltán Micskei, László Balogh et al.)....Pages 460-467 Back Matter ....Pages 469-470