This Article 
 Bibliographic References 
 Add to: 
QDA - A Method for Systematic Informal Program Analysis
June 1994 (vol. 20 no. 6)
pp. 445-462

Formal verification of program properties may be infeasible or impractical, and informal analysis may be sufficient. Informal analysis involves the informal acceptance, by inspection, of the validity of program properties or steps in an analysis. Informal analysis may also involve abstraction. Abstraction can be used to eliminate details and concentrate on more general properties. Abstraction will result in informal analysis if it includes the use of undefined properties. A systematic, informal method for analysis called QDA (Quick Defect Analysis) is described. QDA is a comments analysis process based on facts and hypotheses. Facts are used to create an abstract program model, and hypotheses are selected, nonobvious program properties which are identified as needing verification. Hypotheses are proved from the facts that define an abstraction. QDA is hypothesis-driven in the sense that only those parts of an abstraction that are needed to prove hypotheses are created. The QDA approach was applied to a previously well tested operational flight program (OFP). The QDA method and the results of the OFP experiment are presented. The problems of incomplete or unsound informal analysis are analyzed, the relationship of QDA to other analysis methods is discussed, and suggested improvements to the QDA method are described.

[1] QDA User Guide And Reference Manual. Software Engineering Laboratory, UCSD, Jan. 1992.
[2] W. E. Howden, "Comments analysis and programming errors,"IEEE Trans. software Eng., vol. 16, no. 1, Jan. 1990.
[3] W. E. Howden, "Errors, design properties and functional program tests," inComputer- Program Testing, B. Chandarsakaren and S. Radicci, Eds. Amsterdam, The Netherlands: North Holland, 1981.
[4] E. Soloway et al., "Designing Documentation to Compensate for Delocalized Plans,"Comm. ACM, Nov. 1988, pp. 1,259-1,267.
[5] W. E. Howden and C. Vail, "An informal verification of a critical system," inProc. Fifth Int. Conf. Software Eng. and Applicat., CIGREF, Toulouse, Dec. 1992.
[6] D.C. Luckham,Programming with Specifications: An Introduction to Anna, A Language for Specifying Ada Programs, Texts and Monographs in Computer Science, Springer-Verlag, Oct. 1990.
[7] D. S. Rosenblum, "Towards a method of programming with assertions," inProc. 14th ICSE, IEEE, Melbourne 1992.
[8] H.D. Mills, R.C. Linger, and A.R. Hevner,Principles of Information Systems Analysis and Design, Academic Press, San Diego, 1986.
[9] H. D. Mills, V. R. Basili, J. D. Gannon, and R. Hamlet,Principles of Computer Programming: A Mathematical Approach. Boston, MA: Allyn and Bacon, 1987.
[10] R. Strom and S. Yemini, "Typestate: A programming language concept for enhancing software reliability,"IEEE Trans. Software Eng., vol. SE-12, pp. 157-171, Jan. 1986.
[11] W. Howden,Functional Program Testing and Analysis. New York: Mc-Graw-Hill, 1987.
[12] D. Jackson, "Aspect: An economical bug-detector." inProc. ICSE, vol. 13, IEEE, Houston, 1991.
[13] W. E. Howden, "A general model for static analysis," inProc. 16th Annu. Hawaii Int. Conf. Syst. Sci., Honolulu, HI, 1983.
[14] R. N. Taylor and L. J. Osterweil, "Analysis and testing based on sequencing specifications," inProc. 4th Jerusalem Conf. Inform. Tech., May 1984.
[15] W. Bartussek and D. L. Parnas, "Using assertions about traces to write abstract specifications for software modules," inProc. 2nd Conf. Euro. Cooperation Inform.Berlin, Germany: Springer-Verlag, 1978.
[16] J. McLean, "A formal foundation for the abstract specification of software,"J. ACM, vol. 31, no. 3, pp. 600-627, July 1984.
[17] D. Hoffman and R. Snodgrass, "Trace specifications: Methodology and models,"IEEE Trans. Software Eng., vol. 14, no. 9, Sept. 1988.
[18] P. E. Lauer, P. R. Torrigiani, and M. W. Shields, "COSY--A system specification language based on paths and processes,"Acta Informatica, vol. 12, no. 2, July 1979.
[19] D. C. Luckham, D. P. Helmbold, S. Meldal, D. L. Bryan, and M.A. Habarler, "Task sequencing language for specifying distributed Ada systems (TSL-1)," Rep. CSL-TR-87-334, Comput. Syst. Lab., Stanford Univ., July 1987.
[20] W. E. Riddle, "An approach to software system modeling and analysis,"Comput. Lang., vol. 49, no. 66, 1979.
[21] A. C. Shaw, "Software descriptions with flow expressions."IEEE Trans. Software Eng., vol. SE4-3, May 1978.
[22] R. B. Kieburtz and A. Silberschatz, "Acces-right expressions,"ACM Trans. Prog. Lang. and Syst., vol. 5, Jan. 1983.
[23] R. H. Campbell and A. N. Habermann. "The specification of process synchronization by path expressions." inLecture Notes in Computer Science vol. 16, Operating Systems, Apr. 1974, pp. 89-102.
[24] R. H. Campbell and R. B. Loksatd, "An overview of Path Pascal's design,"SIGPLAN Notices. vol. 15, Sept. 1980.
[25] G. S. Avrunin, L. K. Dillon, J. C. Wileden, and W. E. Riddle, "Constrained expressions: adding analysis capabilities to design methods for concurrent software systems,"IEEE Trans. Software Eng., vol. SE- 12, pp. 278-292, Feb. 1986.
[26] K. M. Olender and L. J. Osterweil, "Cecil: A sequencing constraint language for automatic static analysis generation."IEEE Trans. Software Eng., vol. 16, no. 3, Mar. 1990.
[27] W. E. Howden, C. Vail, and B. Wieand, "Interface error analysis," Software Eng. Lab., Comput. Sci. and Eng., UCSD, 1992.
[28] D. Perry and W. M. Evangelist, "An empirical study of software interface faults--An update," inProc 20th HICSS, vol. 2, 1987.
[29] V. R. Basili and B. T. Perricone, "Software errors and complexity: An empirical investigation,"Commun. ACM, vol. 27, no. 1, p. 42-52, Jan. 1984.
[30] D. E. Perry, "Software interconnection models," inProc. 9th Int. Conf. Software Engineering, Monterey, CA, Mar. 1987, pp. 61-69.
[31] R. Brooks, "Towards a theory of the comprehension of computer programs,"Int. J. of Man-Machine Studies, vol. 18, 1983.
[32] D. N. Card, G. T. Page, and F. E. McGarry, "Evaluating software technologies,"IEEE Trans. Software Eng., vol. SE-13, no. 7, July 1987.
[33] S. McConnell,Code Complete. Redmond, WA: Microsoft Press, 1993.
[34] M. E. Fagan, "Advances in software inspections,"IEEE Trans. Software Eng., vol. SE-12, no. 5, pp. 744-751, July 1986.
[35] P. M. Johnson, "An instrumented approach to improving software quality through formal technical review," inProc. ICSE, vol. 16, IEEE, May 1994.
[36] N. G. Leveson, "Analyzing software safety,"IEEE Trans. Software Eng., vol. SE-9, Sept. 1983.

Index Terms:
program verification; programming theory; formal specification; program debugging; program diagnostics; QDA; systematic informal program analysis; formal verification; program properties; program validity; Quick Defect Analysis; comments analysis; abstract program model; program verification; hypothesis-driven method; operational flight program; specification; code reading
W.E. Howden, B. Wieand, "QDA - A Method for Systematic Informal Program Analysis," IEEE Transactions on Software Engineering, vol. 20, no. 6, pp. 445-462, June 1994, doi:10.1109/32.295893
Usage of this product signifies your acceptance of the Terms of Use.