This Article 
 Bibliographic References 
 Add to: 
SOFL: A Formal Engineering Methodology for Industrial Applications
January 1998 (vol. 24 no. 1)
pp. 24-45

Abstract—Formal methods have yet to achieve wide industrial acceptance for several reasons. They are not well integrated into established industrial software processes, their application requires significant abstraction and mathematical skills, and existing tools do not satisfactorily support the entire formal software development process. We have proposed a language called SOFL (Structured-Object-based-Formal Language) and a SOFL methodology for system development that attempts to address these problems using an integration of formal methods, structured methods and object-oriented methodology. Construction of a system uses structured methods in requirements analysis and specifications, and an object-based methodology during design and implementation stages, with formal methods applied throughout the development in a manner that best suits their capabilities. This paper describes the SOFL methodology, which introduces some substantial changes from current formal methods practice. A comprehensive, practical case study of an actual industrial Residential Suites Management System illustrates how SOFL is used.

[1] S. Liu, V. Stavridou, and B. Dutertre, "The Practice of Formal Methods in Safety Critical Systems," J. Systems and Software, vol. 28, pp. 77-87, 1995.
[2] D. Craigen, S. Gerhart, and T. Ralston, "Formal Methods Reality Check: Industrial Usage," Proc. FME'93: Industrial-Strength Formal Methods, pp. 250-267.Odense, Denmark: Springer-Verlag, Apr. 1993.
[3] H. Saiedian et al., "An Invitation to Formal Methods," Computer, vol. 29, no. 4, Apr. 1996, pp. 16-32.
[4] The VDM-SL Tool Group, "Users Manual for the IFAD VDM-SL Tools," Technical Report IFAD-VDM-4, Inst. of Applied Computer Science, IFAD, Dec. 1994.
[5] A. Bloesch, E. Kazmierczak, and M. Utting, "The Sum Environment in Ergo: A Tutorial," Technical Report 96-22, Software Verification Research Centre, The Univ. of Queensland, Sept. 1996.
[6] J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas, "A Tutorial Introduction to PVS," Proc. WIFT'95: Workshop Industrial-Strength Formal Specification Techniques, Apr. 1995.
[7] D.L. Parnas and D.M. Weiss, "Active Design Reviews: Principles and Practices," Proc. Eighth Int'l Conf. Software Eng., pp. 215-222, Aug. 1985.
[8] M.E. Fagan, "Design and Code Inspections to Reduce Errors in Program Development," IBM Systems J., vol. 15, no. 3, pp. 182-211, 1976.
[9] J. Knight and E.A. Myers, "An Improved Inspection Technique," Comm. ACM, vol. 36, no. 11, pp. 51-61, Nov. 1993.
[10] S. Liu, "Evolution: A More Practical Approach than Refinement for Software Development," Proc. Third IEEE Int'l Conf. Eng. of Complex Computing Systems,Como, Italy, pp. 142-151, IEEE CS Press, Sept. 1997.
[11] P. Stocks and D. Carrington, A Framework for Specification-Based Testing IEEE Trans. Software Eng., vol. 22, no. 11, pp. 777-793, 1996.
[12] E.J. Weyuker, T. Goradia, and A. Singh, "Automatically Generating Test Data from Boolean Specification," IEEE Trans. Software Eng., vol. 20, no. 5, pp. 353-363, May 1994.
[13] A.J. Offutt and S. Liu, "Generating Test Data from SOFL Specifications," J.Systems and Software, to appear.
[14] A. Bloesch, E. Kazmierczak, P. Kearney, and O. Traynor, "Cogito: Methodology and System for Formal Software Development," Int'l J. Software Eng. and Knowledge Eng., vol. 5, no. 4, pp. 599-618, 1995.
[15] S. Liu, "Formal Methods and Intelligent Software Engineering Environments," Technical Report HCU-IS-95-006, Hiroshima City Univ., 1995.
[16] A. Diller, Z: An Introduction to Formal Methods, second edition. New York: John Wiley&Sons, 1994.
[17] J. Dawes, "The VDM-SL Reference Guide," Pitman, 1991.
[18] L.T. Semmens, R.B. France, and T.W.G. Docker, "Integrated Structured Analysis and Formal Specification Techniques," The Computer J., vol. 35, no. 6, 1992.
[19] A. Bryant, "Structured Methodologies and Formal Notations: Developing A Framework for Synthesis and Investigation," Proc. Z User Workshop,Oxford 1989. Springer-Verlag, 1991.
[20] M.D. Fraser et al., "Informal and Formal Requirements Specification Languages: Bridging the Gap," IEEE Trans. Software Eng., vol. 17, no. 5, pp. 454-466, May 1991.
[21] N. Plat, J. van Katwijk, and K. Pronk, "A Case for Structured Analysis/Formal Design," Proc. VDM '91, Lecture Notes in Computer Science No. 551, Springer-Verlag, Berlin, 1991, pp. 81-105.
[22] S. Liu, "A Formal Requirements Specification Method Based on Data Flow Analysis," J. Systems and Software, vol. 21, pp. 141-149, 1993.
[23] S. Liu, "Internal Consistency of FRSM Specifications," J. Systems and Software, vol.. 2, pp. 167-176, May 1995.
[24] E.H. Dürr and J. van Katwijk, "VDM++, A Formal Specification Language for Object Oriented Designs," Proc. Conf. Tools Euro'92 in Technology of Object-Oriented Languages and Systems, Tools 7. Prentice Hall Int'l, 1992.
[25] S.R.L. Meira and A.L.C. Cavalcanti, "Modular Object-Oriented Z Specifications," C.J. van Rijsbergen, ed., Proc. Workshop on Computing Series, Lecture Notes in Computer Science, pp. 173-192.Oxford, UK: Springer-Verlag, 1990.
[26] P. Coad and E. Yourdon, Object-Oriented Design, first edition. Prentice Hall, 1991.
[27] S. Liu and Y. Sun, "Structured Methodology + Object-Oriented Methodology + Formal Methods: Methodology of SOFL," Proc. First IEEE Int'l Conf. Eng. Complex Computer Systems, pp. 137-144,Ft. Landerdale, Fla., IEEE CS Press, Nov. 1995.
[28] K.E. Huff, "Software Process Modeling," A. Wolf and A. Fuggetta, eds., Software Process, vol. 5, Trends in Software: Software Process, pp. 1-24. John Wiley&Sons., 1996.
[29] W.W. Royce, "Managing the Development of Large Software Systems," Proc. IEEE WESCON, pp. 1-9, 1970. Reprinted in R.H. Thayer, ed., IEEE Tutorial on Software Eng. Project Management, 1988.
[30] B. Boehm, "A Spiral Model of Software Development and Enhancement," Computer, May 1988, pp. 61-72.
[31] C. Ho-Stuart and S. Liu, "An Operational Semantics for SOFL," Proc. 1997 Asia-Pacific Software Eng. Conf.,Hong Kong, IEEE CS Press, 1997, to appear.
[32] T. DeMarco, Structured Analysis and System Specification, Yourdon Inc., 1978.
[33] E. Yourdon, Modern Structured Analysis, Prentice Hall, Englewood Cliffs, N.J., 1989.
[34] C. Morgan, Programming from Specifications, Prentice Hall, 1990.
[35] A. Hall, “Using Formal Methods to Develop an ATC Information System,” IEEE Software, vol. 13, no. 2, pp. 66–76, Mar. 1996.
[36] S. Liu and C. Ho-Stuart, "Semi-Automtic Transformation from Formal Specifications to Programs," Proc. Int'l Conf. Eng. Complex Computer Systems, pp. 506-513,Montreal, Quebec, Canada, IEEE CS Press, Oct. 1996.

Index Terms:
Structured methods, object-oriented methodology, formal methods, data flow diagrams, formal languages.
Shaoying Liu, A. Jeff Offutt, Chris Ho-Stuart, Yong Sun, Mitsuru Ohba, "SOFL: A Formal Engineering Methodology for Industrial Applications," IEEE Transactions on Software Engineering, vol. 24, no. 1, pp. 24-45, Jan. 1998, doi:10.1109/32.663996
Usage of this product signifies your acceptance of the Terms of Use.