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.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

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


    Contributors:
    Sokolsky, O. (author) / Younis, M. (author) / Lee, Insup (author) / Kwak, Hee-Hwan (author) / Zhou, J. (author)


    Publication date :

    1998


    Size :

    10 Seiten, 16 Quellen




    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    English




    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 | European Patent Office | 2016

    Free access