Model checking has become a promising automated verification technique in practice. Nevertheless, most existing model checkers are specialized for limited aspects of a system where each of them requires a certain level of expertise to use the tool in the right domain in the right way. Hardly any guideline is available on choosing the right model checker for a particular problem domain, which makes adopting the technique more difficult in practice. Based on the author's prior experience with the use of the symbolic model checker NuSMV on commercial Flight Guidance Systems (FGS) at Rockwell-Collins, the relative benefits and pitfalls of using the explicit model checker SPIN on the same problem are investigated. This has been a question from the beginning of the project with Rockwell-Collins. The challenge includes an efficient use of SPIN for the complex synchronous mode logic with a large number of state variables, where SPIN is known to be not particulary efficient. The author present the way the SPIN model is optimized to avoid the state space explosion problem, which makes SPIN scale up better than NuSMV in the end, and discuss the implication of the result. It will be hoped that the experience can be a useful reference for the future use of model checking in a similar domain.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Model checking flight guidance systems: from synchrony to asynchrony


    Weitere Titelangaben:

    Modellprüfung des Flugleitsystems: der Weg von der synchronen zur asynchronen Überwachung


    Beteiligte:
    Choi, Yunja (Autor:in)


    Erscheinungsdatum :

    2004


    Format / Umfang :

    18 Seiten, 8 Bilder, 25 Quellen



    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch




    Perceptual asynchrony for motion.

    Lo, YT / Zeki, S | BASE | 2014

    Freier Zugriff

    FLIGHT ROUTE GUIDANCE SYSTEM, FLIGHT ROUTE GUIDANCE DEVICE AND FLIGHT ROUTE GUIDANCE METHOD

    NAKAZAWA MITSURU / IWASE HIROAKI | Europäisches Patentamt | 2021

    Freier Zugriff



    Guidance systems in manned space flight

    Cap, S.T. / White, N.P. | Engineering Index Backfile | 1959