Abstract

Automatic Construction of State Invariants from Specifications and Their Application in Software Development

SCR (Software Cost Reduction), a tabular method and notation for specifying software requirements, was introduced in 1978 to document the requirements of the flight program of the U.S. Navy's A-7 aircraft and has been used subsequently in the development of numerous practical software systems. After briefly reviewing the SCR formal semantics and the SCR tools developed at NRL, this talk describes two algorithms for constructing state invariants from SCR specifications and shows how state invariants can be used 1) to validate and to verify requirements specifications using compositional methods and 2) to transform a specification into a form that will lead to more efficient code than the original specification.

Back to Distinguished Lecture Series - Fall 2004 / Spring 2005 Schedule