NASA Formal Methods

1. Front Matter

   PDF

2. DO-333 Certification Case Studies

   • Darren Cofer, Steven Miller

   Pages 1-15

3. A Compositional Monitoring Framework for Hard Real-Time Systems

   • André de Matos Pedro, David Pereira, Luís Miguel Pinho, Jorge Sousa Pinto

   Pages 16-30

4. Leadership Election: An Industrial SoS Application of Compositional Deadlock Verification

   • Pedro R. G. Antonino, Marcel Medeiros Oliveira, Augusto C. A. Sampaio, Klaus E. Kristensen, Jeremy W. Bryans

   Pages 31-45

5. Verification of Certifying Computations through AutoCorres and Simpl

   • Lars Noschinski, Christine Rizkallah, Kurt Mehlhorn

   Pages 46-61

6. Distinguishing Sequences for Partially Specified FSMs

   • Robert M. Hierons, Uraz Cengiz Türker

   Pages 62-76

7. On Proving Recoverability of Smart Electrical Grids

   • Seppo Horsmanheimo, Maryam Kamali, Mikko Kolehmainen, Mats Neovius, Luigia Petre, Mauno Rönkkö et al.

   Pages 77-91

8. Providing Early Warnings of Specification Problems

   • Dustin Hoffman, Aditi Tagore, Diego Zaccai, Bruce W. Weide

   Pages 92-97

9. Mechanized, Compositional Verification of Low-Level Code

   • Björn Bartels, Nils Jähnig

   Pages 98-112

10. Formally Verified Computation of Enclosures of Solutions of Ordinary Differential Equations

    • Fabian Immler

    Pages 113-127

11. On the Quantum Formalization of Coherent Light in HOL

    • Mohamed Yousri Mahmoud, Sofiène Tahar

    Pages 128-142

12. Refinement Types for tla ⁺

    • Stephan Merz, Hernán Vanzetto

    Pages 143-157

13. Using Lightweight Theorem Proving in an Asynchronous Systems Context

    • Matthew Danish, Hongwei Xi

    Pages 158-172

14. JKelloy: A Proof Assistant for Relational Specifications of Java Programs

    • Aboubakr Achraf El Ghazi, Mattias Ulbrich, Christoph Gladisch, Shmuel Tyszberowicz, Mana Taghdiri

    Pages 173-187

15. Verifying Hybrid Systems Involving Transcendental Functions

    • Paul Jackson, Andrew Sogokon, James Bridge, Lawrence Paulson

    Pages 188-202

16. Verifying Nonpolynomial Hybrid Systems by Qualitative Abstraction and Automated Theorem Proving

    • William Denman

    Pages 203-208

17. Combining PVSio with Stateflow

    • Paolo Masci, Yi Zhang, Paul Jones, Patrick Oladimeji, Enrico D’Urso, Cinzia Bernardeschi et al.

    Pages 209-214

18. Qed. Computing What Remains to Be Proved

    • Loïc Correnson

    Pages 215-229

19. Warps and Atomics: Beyond Barrier Synchronization in the Verification of GPU Kernels

    • Ethel Bardsley, Alastair F. Donaldson

    Pages 230-245

20. Testing-Based Compiler Validation for Synchronous Languages

    • Pierre-Loïc Garoche, Falk Howar, Temesghen Kahsai, Xavier Thirioux

    Pages 246-251

This book constitutes the refereed proceedings of the 6th International Symposium on NASA Formal Methods, NFM 2014, held in Houston, TX, USA, April 29 – May 1, 2014. The 20 revised regular papers presented together with 9 short papers were carefully reviewed and selected from 107 submissions. The topics include model checking, theorem proving, static analysis, model-based development, runtime monitoring, formal approaches to fault tolerance, applications of formal methods to aerospace systems, formal analysis of cyber-physical systems, including hybrid and embedded systems, formal methods in systems engineering, modeling, requirements and specifications, requirements generation, specification debugging, formal validation of specifications, use of formal methods in safety cases, use of formal methods in human-machine interaction analysis, formal methods for parallel hardware implementations, use of formal methods in automated software engineering and testing, correct-by-design, design for verification, and property based design techniques, techniques and algorithms for scaling formal methods, e.g., abstraction and symbolic methods, compositional techniques, parallel and distributed techniques, and application of formal methods to emerging technologies.

• embeded systems
• formal methods
• formal verification
• gene regulation networks
• java
• model checking
• real-time systems
• simulation
• software engineering
• static analysis
• theorem proving
• theorem proving

• NASA, Houston, USA

  Julia M. Badger

• Intelligent Systems Division, NASA Ames Research Center, Moffett Field, USA

  Kristin Yvonne Rozier

Policies and ethics