Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
A methodology for assessing the correctness of control programs
Bastani F., Ramamoorthy C. (ed) Computers and Electrical Engineering11 (2-3):115-144,1984.Type:Article
Date Reviewed: Jan 1 1987

This paper is frustrating in that it has a misleading title, contains several misleading comments, and features a substantial, yet irrelevant, example (taking up 11 out of the 30 pages); but, notwithstanding all this criticism, it includes some very interesting material. Indeed, if the paper had been suitably pruned and entitled “The Application of Fuzzy Logic to Estimating the Probability (or Possibility?) of Program Correctness Based on Selective Test Data,” then I would have few qualms about recommending it to the software community.

In my view, the title suggests that the authors are considering the correctness of process control programs; that is, programs which control some (realtime]) process. Indeed, the potentially catastrophic failures cited in their Abstract and Introduction are in process control, but what they really mean is the control component of any program. Moreover, stringing together the contents of the first few sentences, it may be concluded that a program is a control program if its reliability is crucial] The reader is also invited to contemplate the possibility of a system being so complex that its specification may be incorrect and/or incomplete. Since there is no absolute measure of correctness, we can never logically allow the notion of an incorrect specification. (It’s like accusing someone of asking the wrong question--it may not be the one which was intended, but it is just as valid]) In the context of this paper, incompleteness means failure to specify what action is to be taken in all situations; hence, the results may be undefined or may be non-deterministic, but again such specifications are perfectly valid and (logically) acceptable.

The real problem is, “Given a complex specification and a program, the sizes of which rule out (with current program proving technology) a full verification proof, how can suitable test data be chosen for the system and what is the probability that successful results from this data will infer correctness of the program?”

Disregarding the diversionary amble through the “well-known” KWIC index generator program, Section 3 of the paper considers how a computation may be split into equivalence classes of “similar” computations (each being subjected to the “same” control flow). Correctness is then estimated by considering each of these classes together with the correctness of the decision procedure that selects the class into which a particular input falls. Since a degree of uncertainty is present throughout the analysis (allowing for the possibility of error), fuzzy mathematics is used throughout (see [1]). The reader will also find it useful to consult an earlier paper by Bastani [2], where details of the formulas used here, and those for less straightforward cases such as loops, are given.

Several questionable assumptions are made: (1) concerning the presence or absence of errors in “thoroughly tested” software; (2) about how one transforms ranges of data values onto the interval [0,1] (for use in probability/possibility calculations); and (3) regarding how errors are then distributed (uniformly?) over this interval. The calculations are then applied to a calendar problem which, although not concerned with process control and computationally rather simple, is of an appropriate size to demonstrate the methodology proposed.

The whole area of software reliability and metrics, and their relationship to program verification, is of crucial importance. However, there is currently a substantial gulf between the theory (in which no incorrect program is acceptable) and practice (in which programs are still tested by small finite amounts of data). The method described in this paper is undoubtedly an important plank in bridging this gap.

While the inexperienced reader may have difficulty in sorting out the salient material in this paper, it is to be welcomed as a supplement to the earlier conference paper by Bastani [2].

Reviewer:  D. J. Cooke Review #: CR109855
1) Zadeh, L. A.Fuzzy sets and information granularity, in Advances in fuzzy set theory and application, M. M. Gupta, R. D. Ragade, and R. R. Yager (Eds.), Elsevier North-Holland, New York, 1979.
2) Bastani, F. B.On the uncertainty in the correctness of computer programs, in Proc. of COMPSAC ’82, Chicago, 1982, 109-118.
Bookmark and Share
 
Correctness Proofs (D.2.4 ... )
 
 
Mathematical Logic (F.4.1 )
 
 
Metrics (D.2.8 )
 
 
Testing And Debugging (D.2.5 )
 
Would you recommend this review?
yes
no
Other reviews under "Correctness Proofs": Date
Using symbolic execution for verification of Ada tasking programs
Dillon L. (ed) ACM Transactions on Programming Languages and Systems 22(6): 643-669, 2000. Type: Article
Jul 1 1991
Reasoning about programs (videotape)
Dijkstra E. (ed), University Video Communications, Stanford, CA, 1990. Type: Book
Dec 1 1992
Error-free software
Baber R., John Wiley & Sons, Inc., New York, NY, 1991. Type: Book (9780471930167)
May 1 1994
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy