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

DOI10.1007/s10703-006-0027-9zbMath1111.68502OpenAlexW2000117665MaRDI QIDQ883136

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)

Uses Software

• SPIN
• NuSMV
• Java PathFinder
• LUSTRE
• Esterel

Cites Work

• The Esterel synchronous programming language: Design, semantics, implementation
• Slicing software for model construction
• Model checking JAVA programs using JAVA PathFinder
• Program Slicing
• Unnamed Item
• Unnamed Item

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