NASA Formal Methods Symposium, May 2017
This paper describes current progress on SpeAR, a novel tool for capturing and analyzing requirements in a domain specific language designed to read like natural language. Using SpeAR, system engineers capture requirements, environmental assumptions, and critical system properties using the formal semantics of Past LTL. SpeAR analyzes requirements for logical consistency and uses model checking to prove that assumptions and requirements entail stated properties. These analyses build confidence in the correctness of the formally captured requirements.