Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning

DOI10.1007/S10472-014-9408-8zbMATH Open1298.68063OpenAlexW2095473904MaRDI QIDQ457250FDOQ457250

Klaus Havelund, Gerard J. Holzmann, Alex Groce, Rajeev Joshi, Ru-Gang Xu

Publication date: 26 September 2014

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-014-9408-8

Recommendations

• Computer Aided Verification
• scientific article; zbMATH DE number 1927410
• Extending Model Checking with Dynamic Analysis
• From NuSMV to SPIN: Experiences with model checking flight guidance systems
• Experimental evaluation of verification and validation tools on Martian Rover software

zbMATH Keywords

verificationtestingmodel checkingformal prooffile systemsflight software

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Software, source code, etc. for problems pertaining to fluid mechanics (76-04)

Cites Work

• Theory and Applications of Satisfiability Testing
• Java-MaC: A run-time assurance approach for Java programs
• Learning regular sets from queries and counterexamples
• Isabelle/HOL. A proof assistant for higher-order logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Symbolic execution and program testing
• Title not available (Why is that?)
• Lazy abstraction
• Tools and Algorithms for the Construction and Analysis of Systems
• Introduction to Software Testing
• Rule Systems for Run-time Monitoring: from EAGLE to RULER
• Title not available (Why is that?)
• Tools and Algorithms for the Construction and Analysis of Systems
• Title not available (Why is that?)
• A mini challenge: build a verifiable filesystem
• Types, bytes, and separation logic
• Testing Programs with the Aid of a Compiler
• Software is different
• Title not available (Why is that?)
• Model Checking Software
• Extending Model Checking with Dynamic Analysis
• On the Synthesis of Finite-State Machines from Samples of Their Behavior

Cited In (4)

• FM 2005: Formal Methods
• Title not available (Why is that?)
• Title not available (Why is that?)
• Computer Aided Verification

Uses Software

• ACL2
• CUTE
• MiniSat
• Isabelle/HOL
• SPIN
• z3
• KLEE
• Bogor
• Chaff
• Limmat
• DART
• QuickCheck
• Bandera
• CBMC
• SPARK Pro
• Nighthawk
• JCrasher
• GDB
• seL4
• CodeSonar
• Klockwork
• EXPLODE
• CIL
• STP

This page was built for publication: Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q457250)