This Article 
 Bibliographic References 
 Add to: 
Formal Methods Application: An Empirical Tale of Software Development
March 2002 (vol. 28 no. 3)
pp. 308-320

The development of an elevator scheduling system by undergraduate students is presented. The development was performed by 20 teams of undergraduate students, divided into two groups. One group produced specifications by employing a formal method that involves only first-order logic. The other group used no formal analysis. The solutions of the groups are compared using the metrics of code correctness, conciseness, and complexity. Particular attention is paid to a subset of the formal methods group which provided a full verification of their implementation. Their results are compared to other published formal solutions. The formal methods group's solutions are found to be far more correct than the nonformal solutions.

[1] J.P. Bowen and M.G. Hinchey, "Ten Commandments of Formal Methods," Computer, vol. 28, no. 4, Apr. 1995, pp. 56-63.
[2] G. Booch, Object-Oriented Analysis and Design with Applications, Addison-Wesley, Reading, Mass., 1994.
[3] L. Christensen, Experimental Methodology. Allyn and Bacon, 1977.
[4] E. Cohen, Programming in the 1990s: An Introduction to the Calculation of Programs. Springer-Verlag, 1990.
[5] D.T. Campbell and J.C. Stanley, Experimental and Quasi-Experimental Designs for Research. Houghton Mifflin, 1963.
[6] E.W. Dijkstra, A Discipline of Programming.Englewood Cliffs, N.J.: Prentice Hall, 1976.
[7] E. Dijkstra and C. Scholten, Predicate Calculus and Program Semantics. Springer-Verlag, 1989.
[8] Anthony Hall, "Seven Myths of Formal Methods," IEEE Software, vol. 7, p. 13, Sept. 1990.
[9] IEEE, Proc. Int'l Workshop Software Specification and Design, 1987.
[10] J. Rumbaugh, I. Jacobson, and G. Booch, The Unified Modeling Language Reference Manual. Addison-Wesley, 1999.
[11] Microsoft, Microsoft Visual C++ MFC Library Reference, vol. 1,Microsoft Press, 1997.
[12] H. Saiedian et al., "An Invitation to Formal Methods," Computer, vol. 29, no. 4, Apr. 1996, pp. 16-32.
[13] M.D. Schwartz and N.M. Delisle, “Specifying a Lift Control System with CSP,” Proc. IEEE Workshop Software Specification and Design, 1987.
[14] ACM, Proc. 29th SIGCSE Technical Symp. Computer Science Education, 1998.
[15] A.E.K. Sobel, “Empirical Results of a Software Engineering Curriculum Incorporating Formal Methods,” ACM Inroads, vol. 32, no. 1, pp. 157–161, Mar. 2000.
[16] A.E.K. Sobel, “Emphasizing Formal Analysis in a Software Engineering Curriculum,” IEEE Trans. Education, May 2001.
[17] B. Stroustrup, The C++ Programming Language. third ed. Addison-Wesley, 1997.
[18] J.C.P. Woodcock, S. King, and I.H. Sorensen, “Mathematics for Specification and Design: The Problem with Lifts...,” Proc. IEEE Workshop Software Specification and Design, 1987.
[19], 2002.

Index Terms:
formal methods, software specifications, software engineering curriculum
A.E. Kelley Sobel, M.R. Clarkson, "Formal Methods Application: An Empirical Tale of Software Development," IEEE Transactions on Software Engineering, vol. 28, no. 3, pp. 308-320, March 2002, doi:10.1109/32.991322
Usage of this product signifies your acceptance of the Terms of Use.