Formal methods have been widely recognized as effective techniques to uncover design errors that could be missed by a conventional software engineering process. The paper describes the authors' experience with using formal methods in analyzing the redundancy management system (RMS) for a space launch vehicle. RMS is developed by AlliedSignal Inc. for the avionics of NASA's new space shuttle, called VentureStar, that meets the expectations for space missions in the 21st century. A process algebraic formalism is used to construct a formal specification based on the actual RMS design specifications. Analysis is performed using PARAGON, a toolset for formal specification and verification of distributed real-time systems. A number of real-time and fault-tolerance properties were verified, allowing some errors in the RMS pseudocode to be detected. The paper discusses the translation of the RMS specification into process algebra formal notation and results of the formal verification.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Verification of the redundancy management system for space launch vehicle: a case study


    Beteiligte:
    Sokolsky, O. (Autor:in) / Younis, M. (Autor:in) / Lee, Insup (Autor:in) / Kwak, Hee-Hwan (Autor:in) / Zhou, J. (Autor:in)


    Erscheinungsdatum :

    1998


    Format / Umfang :

    10 Seiten, 16 Quellen




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch




    The space shuttle launch vehicle aerodynamic verification challenges

    Wallace, R. O. / Austin, L. D. / Hondros, J. G. et al. | NTRS | 1985



    Verification of redundancy management design

    Gelderloos, H. C. / Wilson, D. V. | NTRS | 1978


    Design and Verification of Launch and Space Vehicle Structures

    Kabe, A. / AIAA; ASME; ASCE | British Library Conference Proceedings | 1998


    Multiple space vehicle launch system

    ASTON RICHARD W / TOMZYNSKA ANNA M / CAPLIN GLENN N | Europäisches Patentamt | 2022

    Freier Zugriff