This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Rapid Application of Lightweight Formal Methods for Consistency Analyses
November 1998 (vol. 24 no. 11)
pp. 949-959

Abstract—Lightweight formal methods promise to yield modest analysis results in an extremely rapid manner. To fulfill this promise, they must be able to work with existing information sources, be able to analyze for manifestly desirable properties, be highly automated (especially if dealing with voluminous amounts of information), and be readily customizable and flexible in the face of emerging needs and understanding. Two pilot studies investigate the feasibility of lightweight formal methods that employ a database as the underlying reasoning engine to perform the analyses. The first study concerns aspects of software module interfaces, the second test logs' adherence to required and expected conditions.

[1] J.F. Allen, “Maintaining Knowledge about Temporal Intervals,” Comm. ACM, vol. 26, no. 11, pp. 832–843, 1983.
[2] B. Boehm, Software Engineering Economics, Prentice Hall, Upper Saddle River, N.J., 1981, pp. 533-535.
[3] D. Cohen, "Compiling Complex Database Transition Triggersm," Proc. ACM SIGMOD Int'l Conf. Management of Data, pp. 225-234,Portland, Ore., ACM Press, 1989.
[4] L.K. Dillon and Q. Yu, “Oracles for Checking Temporal Properties of Concurrent Systems,” Proc. Symp. Foundations of Software Eng., pp. 140–153, Dec. 1994.
[5] S. Easterbrook, R. Lutz, R. Covington, Y. Ampo, and D. Hamilton, "Experiences Using Lightweight Formal Methods for Requirements Modeling," IEEE Trans. Software Eng., vol. 24, no. 1, Jan. 1998.
[6] A. Finkelstein, J. Kramer, B. Nuseibeh, L. Finkelstein, and M. Goedicke, "Viewpoints: A Framework for Integrating Multiple Perspectives in System Development," Int'l J. Software Eng. and Knowledge Eng., vol. 2, no. 1, pp. 31-58, Mar. 1992.
[7] C.L. Heitmeyer, R.D. Jeffords, and B.G. Labaw, "Automated Consistency Checking of Requirements Specifications," ACM Trans. Software Eng. and Methodology, pp. 231-261, vol. 5, July 1996.
[8] D. Jackson and J. Wing, "Lightweight Formal Methods," Computer, pp. 21-22, Apr. 1996.
[9] N.C. Levenson, M.P.E. Heimdahl, H. Hildreth, and J.D. Reese, "Requirements Specification for Process-Control Systems," IEEE Trans. Software Eng., vol. 20, no. 9, pp. 684-707, Sept. 1994.
[10] R. Lutz and J. Wong, "Detecting Unsafe Error Recovery Schedules," IEEE Trans. Software Eng., vol. 18, no. 8, pp. 749-760, 1992.
[11] R. Lutz, "Analyzing Software Requirements Errors in Safety-Critical, Embedded Systems," Proc. IEEE Int'l Symp. Requirements Eng., RE '93, pp. 126-133,San Diego, Calif., Jan. 1993.
[12] S. Owry, J. Rushby, and N. Shankar, "Integration in PVS: Tables, Types, and Model Checking," Tools and Algorithms for the Construction and Analysis of Systems, TACAS'97, Enschede: The Netherlands, 1997.
[13] Joint Proc. SIGSOFT'96 Workshops, Part II: Proc. Int'l Workshop Multiple Perspectives in Software Development, L. Vidal, A. Finkelstein, G. Spanoudakis, and A. Wolf, eds., ACM 1996.

Index Terms:
Consistency checking, formal methods, interface checking, test-log checking, database-based analysis, NASA.
Citation:
Martin S. Feather, "Rapid Application of Lightweight Formal Methods for Consistency Analyses," IEEE Transactions on Software Engineering, vol. 24, no. 11, pp. 949-959, Nov. 1998, doi:10.1109/32.730544
Usage of this product signifies your acceptance of the Terms of Use.