Power and limitations of formal methods for software fabrication: Thirty years later

Authors

  • Edgar Serna M. Corporación Universitaria Remington
  • Alexei Serna A. Corporación Universitaria Remington

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.

References

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.

Downloads

Published

2017-05-09

How to Cite

Serna M., E., & Serna A., A. (2017). Power and limitations of formal methods for software fabrication: Thirty years later. Informatica, 41(3). Retrieved from https://puffbird.ijs.si/index.php/informatica/article/view/1534

Issue

Vol. 41 No. 3 (2017)

Section

Regular papers

License

I assign to Informatica, An International Journal of Computing and Informatics ("Journal") the copyright in the manuscript identified above and any additional material (figures, tables, illustrations, software or other information intended for publication) submitted as part of or as a supplement to the manuscript ("Paper") in all forms and media throughout the world, in all languages, for the full term of copyright, effective when and if the article is accepted for publication. This transfer includes the right to reproduce and/or to distribute the Paper to other journals or digital libraries in electronic and online forms and systems.

I understand that I retain the rights to use the pre-prints, off-prints, accepted manuscript and published journal Paper for personal use, scholarly purposes and internal institutional use.

In certain cases, I can ask for retaining the publishing rights of the Paper. The Journal can permit or deny the request for publishing rights, to which I fully agree.

I declare that the submitted Paper is original, has been written by the stated authors and has not been published elsewhere nor is currently being considered for publication by any other journal and will not be submitted for such review while under review by this Journal.  The Paper contains no material that violates proprietary rights of any other person or entity. I have obtained written permission from copyright owners for any excerpts from copyrighted works that are included and have credited the sources in my article. I have informed the co-author(s) of the terms of this publishing agreement.


Copyright ©  Slovenian Society Informatika