Power and limitations of formal methods for software fabrication: Thirty years later
Abstract
In 1987, Michael Jackson presented his work "Power and Limitations of Formal methods for software fabrication" at the AIT Conference, which analyzed the advantages and limitations of formal methods up to that time. His conclusion was that formal methods had undoubted capabilities and advantages, but they also had serious limitations that prevented their widespread acceptance and adoption. The aim of this paper is to present the current context of formal methods compared with what Jackson described three decades ago. A tour of the strengths and limitations of formal methods is taken through a review of literature in the timeline of the past thirty years. The conclusion is that little progress has been made on this issue in relation to the situation presented by Jackson, and formal methods still need more work from academia, industry and the community.
Full Text:
PDFReferences
Cohen, B. (1995). A brief history of ‘Formal Methods’. Formal aspects of computing, 1(3), 1-10.
Neugebauer, O. (1969). The Exact Sciences in Antiquity. USA: Dover Publications.
Serna, M.E. (Ed.) (2015). Avances en ingeniería. Medellín: Editorial Instituto Antioqueño de Investigación.
Dani, S. (1993). 'Vedic Mathematics': Myth and Reality. Economic and Political Weekly, 28(31), 1577-1580.
Dowling, P. (1998). The Sociology of Mathematics Education: Mathematical Myths/Pedagogic Texts. London: Falmer Press.
Holloway, C. (1997). Why Engineers Should Consider Formal Methods. 16th Digital Avionics Systems Conference. Irvine, USA, 16-22.
Butler, R. (2001). What is Formal Methods? NASA. Online [Aug 2016].
Naur, P. & Randell, B. (1968). Software Engineering. Scientific Affairs Division NATO. Germany, Garmisch.
Bjørner, D. & Havelund, K. (2014). 40 years of formal methods- Some obstacles and some possibilities? Lecture Notes in Computer Science, 8442, 42-61.
Jackson, M. (1987). Power and limitations of formal methods for software fabrication. Journal of Information Technology, 2(2), 1-6.
Hall, A. (1991). Seven Myths of formal methods. IEEE Software, 7(5), 11-19.
Gaudel, M. (1991). Advantages and limits of formal approaches for ultra-high dependability. Proceedings of the Sixth International Workshop on Software Specification and Design. Como, Italy, 237-241.
Young, W. (1991). Formal Methods versus Software Engineering - Is there a conflict? Fourth Testing, Analysis, and Verification Symposium. Victoria, Canada, 188-899.
Barroca, L. & McDermid, J. (1992). Formal Methods: Use and relevance for the development of safety critical systems. The Computer Journal, 35(6), 579-599.
Vienneau, R. (1993). A review of Formal Methods. Technical Report, Kaman Science Corporation.
Gerhart, S., Craigen, D. & Ralston, T. (1994). Experience with Formal Methods in Critical Systems. IEEE Software, 11(1), 21-28.
Liu, S. & Adams, R. (1995). Limitations of formal methods and an approach to improvement. Proceedings Asia Pacific Software Engineering Conference. Brisbane, Australia, 498-507.
Craigen, D., Gerhart, S. & Ralston, T. (1995). Industrial applications of formal methods to model, design and analyze computer systems - An international survey. New Jersey: Noyes Data.
Bowen, J. & Hinchey, M. (1995). Seven more myths of formal methods - Dispelling industrial prejudices. Lecture Notes in Computer Science, 873, 105-117.
Rushby, J. (1996). Mechanized Formal Methods: Progress and prospects. Lecture Notes in Computer Science, 1180, 43-51.
Easterbrook, S. et al. (1996). Experiences using formal methods for requirements modeling. Technical Report NASA-CR-203085.
Kneuper, R. (1997). Limits of Formal Methods. Formal Aspects of Computing, 3(1), 1-16.
Knight, J., Dejong, C., Gibble, M. & Nakano, L. (1997). Why are formal methods not used more widely? Fourth NASA Langley Formal Methods Workshop. Virginia, USA, 1-12.
Wing, J. (1998). A symbiotic relationship between formal methods and security. Proceedings Conf. on Computer Security, Dep. and Assu: From Needs to Solutions. Williamsburg, USA, 26-38
Jones, S., Till, D. & Wrightson, A. (1998). Formal Methods and Requirements Engineering - Challenges and Synergies. Journal of Systems and Software, 40(3), 263-273.
Heylighen, F. (1999). Advantages and limitations of formal expression. Foundations of Science, 4(1), 25-56.
Wordsworth, J. (1999). Getting the best from formal methods. Information and Software Technology, 41, 1027-1032.
Broadfoot, G. & Broadfoot, P. (2003). Academia and industry meet - Some experiences of formal methods in practice. Tenth Asia-Pacific Software Engine. Conference. Chiang Mai, China, 49-58.
Amey, P. (2004). Dear Sir, yours faithfully - An everyday story of formality. In Redmill, F. & Anderson, T. (Eds.), Practical Elements of Safety. UK: Springer, 3-15.
Edmonds, B. and Bryson, J. (2004). The insufficiency of Formal Design Methods. Proceedings Third International Joint Conference on Autonomous Agents and Multiagent Systems. New York, USA, 938-945.
Gogolla, M. (2004). Benefits and problems of Formal Methods. LNCS, 3063, 1-15.
Glass, R. (2004). The mystery of Formal Methods Disuse. Communications of the ACM, 47(8), 15-17.
Hall, A. (2005). Realising the benefits of Formal Methods. LNCS, 3785, 1-4.
Sommerville, I. (2009). Software Engineering. New York: Pearson.
Parnas, D. (2010). Really rethinking ‘formal methods’. Computer, 34(1), 28-34.
IET. (2011). Formal Methods. The IET.
Batra, M., Malik, A. & DAVE, M. (2013). Formal methods - Benefits, challenges and future direction. Journal of Global Research in Comp. Scien., 45, 21-25.
Fitzgerald, J. (2013). Industrial deployment of formal methods: Trends and challenges. In Romanovsky, A. and Thomas, T. (Eds.), Industrial Deployment of System Engineering Methods. Berlin: Springer, 123-143.
Ishikawa, F., Yoshioka, N. & Tanabe, Y. (2015). Keys and roles of formal methods education for industry: 10 Year experience with Top SE Program. Proceedings First Workshop on Formal Methods in SEE & Training. Oslo, Norway, 35-42.
Mayo, J., Armstrong, R. & Hulette, G. (2015). Digital System Robustness via Design Constraints: The Lesson of Formal Methods. In 9th IEEE International Systems Conference. Vancouver, Canada, 109-114.
Gross, K., Fifarek, A. & Hoffman, J. (2016). Incremental Formal Methods Based Design Approach Demonstrated on a Coupled Tanks Control System. Proceedings 17th International Symposium on High Assurance Systems Engineering. Orlando, USA, 181-188.
Alvear, A. & Quintero, G. (2015). Integrating software development techniques, usability, and agile methodologies. Actas de Ingeniería 1, 94-103.
Polansky, J. & Sinclair, M. (2014). The importance of training in formal methods in Software Engineering. Revista Antioqueña de las Ciencias Computacionales y la Ingeniería de Software (RACCIS), 4(2), 52-56.
Serna, M.E. (2013). Prueba funcional del software - Un proceso de Verificación constante. Medellín: Editorial Instituto Antioqueño de Investigación.
Serna, M.E. & Serna, A.A. (2013). Is it in crisis engineering in the world? A literature review. Revista Facultad de Ingeniería, 66, 197-206.
Tucker, A., Kelemen, C. & Bruce, K. (2001). Our curriculum has become Math-Phobic! Proceedings 32th Technical Symposium on Computer Science Education. Charlotte, USA, 243-247.
This work is licensed under a Creative Commons Attribution 3.0 License.