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.
Formal Verification Toolkit for Requirements and Early Design Stages
NASA Formal Methods Symposium ; 2012 ; Norfolk, VA, United States
01.01.2011
Aufsatz (Konferenz)
Keine Angabe
Englisch
A formal method for early spacecraft design verification
| IEEE | 2013
Formal verification of safety requirements on complex systems
| Tema Archiv | 1996
Formal Verification in Early Mission Planning
| Deutsches Zentrum für Luft- und Raumfahrt (DLR) | 2012
Formal Verification in Early Mission Planning
| Deutsches Zentrum für Luft- und Raumfahrt (DLR) | 2012