Computer Science

Colloquium Details

Automatic Construction of State Invariants and Their Application in Software Development

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 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 may be used 1) to validate and verify requirements specifications and 2) to optimize code.

Biography

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 co-editor of the book, Formal Methods for Real-Time Computing, published by John Wiley. Her research interests are in formal specification and formal analysis of software, requirements specification, and real-time computing.