FM'99 User Group Meeting


PVS Specification and Verification System

Dave Stringer-Calvert

User Group Presentation

PVS-based Verification of SCR-style Requirements: Experience and Wish List

Tae-Ho Kim and Sung-Deok Cha
Department of Computer Science,
Korea Advanced Institute of Science and Technology (KAIST)
373-1, Kusong-dong, Yusong-gu, Taejon, Korea
e-mail:{ thkim, cha}

Software requirements can largely be classified as either structural or functional. The former, application independent, investigates whether definitions and uses of variables, functions, and function groups are consistent, while the latter examines if requirements accurately reflect users' needs. We used inspection technique to validate software requirements specification (SRS) for Wolsung SDS2 which is a shutdown system for nuclear power plant in Korea. SRS is nearly 400 pages long and is written in SCR-style. Our experience indicates that inspection is ineffective in detecting errors violating structural properties whose examples include the followings:

Inspecting large volume of document for consistency among information scattered among various pages is not only labor-intensive but also intellectually uninteresting. Inspection becomes a less attractive option especially if requirements are subject to several but minor revisions. In order to relieve the inspection teams of burdens of having to carrying out tedious tasks, we have developed software to capture and translate information relevant to structural properties of SCR-style specification into valid PVS theorems. The tool provides graphical interface to allow entry and editing of SCR-style specification. Structural properties are captured in PVS theorems, and the PVS proof checker commands are used to automatically carry out much, but not all, of the proof. Our experience convincingly demonstrated that PVS-based verification of structural properties is a powerful and cost-effective approach to the verification of structural properties.

Additionally, as we use PVS on verification of Wolsung SDS2 software requirements, we have come to develop the following wish list:

There is no doubt that PVS is useful in developing and verifying safety-critical software. Unfortunately, it is also true that becoming a power user of PVS requires significant investment on one's time and technical expertise. Enhancements suggested above could make the next version of PVS user-friendlier for ordinary users.

Dave Stringer-Calvert (