From NuSMV to SPIN: Experiences with model checking flight guidance systems

DOI10.1007/S10703-006-0027-9MaRDI QIDQ883136zbMATH OpenOpenAlexFDO

Authors Yunja Choi

Publication date 31 May 2007

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-006-0027-9

zbMATH Keywords

SPINModel checkingNuSMVFlight guidance systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 2087633
• scientific article; zbMATH DE number 1633145
• scientific article; zbMATH DE number 1487860
• scientific article; zbMATH DE number 2080188
• Principles of the SPIN model checker. Foreword by Gerard J. Holzmann

Cites work

• scientific article; zbMATH DE number 2087633 (Why is no real title available?)
• scientific article; zbMATH DE number 2102731 (Why is no real title available?)
• Model checking JAVA programs using JAVA PathFinder
• Program Slicing
• Slicing software for model construction
• The Esterel synchronous programming language: Design, semantics, implementation

Cited in

(3)

• scientific article; zbMATH DE number 2087633 (Why is no real title available?)
• scientific article; zbMATH DE number 1630128 (Why is no real title available?)
• Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning

Describes a project that uses

Uses Software

• Esterel
• LUSTRE
• Java PathFinder
• NuSMV
• SPIN

This page was built for publication: From NuSMV to SPIN: Experiences with model checking flight guidance systems

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