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
2011-01-01
Conference paper
No indication
English
A formal method for early spacecraft design verification
IEEE | 2013
|Formal verification of safety requirements on complex systems
Tema Archive | 1996
|