Efficient flight software development from natural language requirements needs an effective way to test designs earlier in the software design cycle. A method to automatically derive logical safety constraints and the design state space from natural language requirements is described. The constraints can then be checked using a logical consistency checker and also be used in a symbolic model checker to verify the early design of the system. This method was used to verify a hybrid control design for the suit ports on NASA Johnson Space Center's Space Exploration Vehicle against safety requirements.


    Access

    Access via TIB

    Check availability in my library


    Export, share and cite



    Title :

    Formal Verification Toolkit for Requirements and Early Design Stages


    Contributors:

    Conference:

    NASA Formal Methods Symposium ; 2012 ; Norfolk, VA, United States


    Publication date :

    2011-01-01


    Type of media :

    Conference paper


    Type of material :

    No indication


    Language :

    English





    A formal method for early spacecraft design verification

    Fischer, Philipp M. / Ludtke, Daniel / Schaus, Volker et al. | IEEE | 2013


    Formal verification of safety requirements on complex systems

    Bernardeschi, C. / Fantechi, A. / Gnesi, S. | Tema Archive | 1996


    Formal Verification in Early Mission Planning

    Fischer, Philipp M. / Lüdtke, Daniel / Schaus, Volker et al. | German Aerospace Center (DLR) | 2012

    Free access

    Formal Verification in Early Mission Planning

    Fischer, Philipp M. / Lüdtke, Daniel / Schaus, Volker et al. | German Aerospace Center (DLR) | 2012

    Free access