PVS
Specification and Verification System
Dave Stringer-Calvert
Email:
dave_sc@csl.sri.com
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}@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)