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

DOI10.1007/S10703-006-0027-9zbMATH Open1111.68502OpenAlexW2000117665MaRDI QIDQ883136FDOQ883136

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)

Cites Work

• The Esterel synchronous programming language: Design, semantics, implementation
• Title not available (Why is that?)
• Program Slicing
• Model checking JAVA programs using JAVA PathFinder
• Slicing software for model construction
• Title not available (Why is that?)

Cited In (2)

• Title not available (Why is that?)
• Title not available (Why is that?)

Uses Software

• SPIN
• NuSMV
• Java PathFinder
• LUSTRE
• Esterel

   Recommendations

• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Principles of the SPIN model checker. Foreword by Gerard J. Holzmann 👍 👎

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)