Dave Stringer-Calvert

Email:
*dave_sc@csl.sri.com*

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}@salmosa.kaist.ac.kr

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:

- All internal data flows must be generated from source and consumed by target modules.
- No circular dependencies exist among data flows.
- All data flows declared in higher-levels of function overview diagrams (FOD), a notation similar to DFD, are consistent with the ones defined in lower-levels.
- Data-flows of one function are consistent with the input-output relation written in tabular notation.

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:

**Instantiations:**Generally speaking, PVS cannot always decide which values of x are satisfied in a theorem (e.g.`EXISTS (x:t): p(x)`). Therefore, we must manually instantiate existentially quantified variables (e.g.`(inst - "3")`). However, if`p(x)`is a first order logic and if the domain of a variable`x`is finite, PVS can and should be extended to prove it automatically by enumerating all elements of`x`and by checking whether the value of`p(x)`for any`x`is true.**Arithmetic operations:**Even though PVS supports arithmetic decision procedures, it cannot solve equations. Perhaps PVS could be extended to use numerical analysis methods to solve equations with existence quantifier and arithmetic expression such as`EXISTS (x:int): x < 3`.**Complex proof commands:**In the PVS prover, commands such as`(grind)`and`(induct-and-simplify)`are quite powerful. However, they are carried out silently or generate inscrutable messages. Should an attempt to prove a theorem using complex proof commands fail, users find it difficult to investigate the cause of failures. Moreover, users may not modify sub-procedure of the complex proof command and solicit useful information from the failed proof.**Loosely coupled graphical user interaction (GUI) environment:**By using Tcl/Tk, PVS supports graphical display mechanism without handling users' inputs through display. Wouldn't it be wonderful if the next generation of PVS comes with WIMP interface that is intuitive and easy to use?**Closed system:**Integration of Tcl/Tk with the PVS prover was done. However, the connector is implemented in LISP, and it is laborious and time-consuming. For easily and seamlessly integrating PVS with other tools such as SCR-to-PVS translator we developed, PVS should provide API (Application Program Interface) for other programming languages such as C, C++, Java, ML, and so on.

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 (dave_sc@csl.sri.com)