Constance Heitmeyer: Towards Kinder, Gentler Formal Methods: Automatic Construction and Application of State Invariants

Abstract: SCR, 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. Since its introduction, SCR has been used in the development of numerous practical systems, including a telephone switching network, control software for nuclear power plants, and the flight programs of other avionics systems, including Lockheed's C-130J aircraft. To provide formal underpinnings for SCR and to facilitate formal analysis of SCR specifications, NRL has developed a state-based formal semantics for the SCR notation and built several tools based on the semantics for checking SCR specifications for properties of interest. This talk briefly reviews SCR's state-machine semantics and the SCR tools and then describes two algorithms for constructing state invariants from SCR specifications. It also shows how state invariants can be used in the validation, verification, and optimization of software.

CV: Connie Heitmeyer heads the Software Engineering Section of the Naval Research Laboratory's Center for High Assurance Computer Systems. She serves on the editorial boards of the Real Time Systems Journal, the Requirements Engineering Journal, and the Journal on Software and System Modeling, and was recently invited to serve as an Associate Editor of the ACM Transactions on Software Engineering and Methodology. She is also a member of the Steering Committee of IFIP Working Group 2.9 on Software Requirements. Her research interests are in formal specification and formal analysis of software, requirements specification, and real-time computing.