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