Skip to main content
SpringerLink
Log in

From Formal Techniques to Well-Founded Software Development Methods

  • Chapter
Book cover Formal Methods at the Crossroads. From Panacea to Foundational Support

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2757))

Abstract

We look at the main issue of the Colloquium “Formal Methods at the Crossroads from Panacea to Foundational Support” reflecting on our rather long experience of active engagement in the development and use of formal techniques. In the years, we have become convinced of the necessity of an approach more concerned with the real needs of the software development practice. Consequently, we have shifted our work to include methodological aspects, learning a lot from the software engineering practices and principles.

After motivating our current position, mainly reflecting on our own experience, we suggest a Virtuous Cycle for the formal techniques having the chance of a real impact on the software development practices. Then, to provide some concrete illustration of the suggested principles, we propose and advocate a strategy that we call Well-Founded Software Development Methods, of which we outline two instantiations.

Work supported by the Italian National Project SAHARA (Architetture Software per infrastrutture di rete ad accesso eterogeneo).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Brückner, B., Mosses, P.D., Sannella, D., Tarlecki, A.: CASL: the Common Algebraic Specification Language. T.C.S. 286(2), 153–196 (2002)

    Article  MATH  Google Scholar 

  2. Astesiano, E., Krieg-Brückner, B., Kreowski, H.-J. (eds.): IFIP WG 1.3 Book on Algebraic Foundations of System Specification. Springer, Heidelberg (1999)

    Google Scholar 

  3. Astesiano, E., Reggio, G.: Direct Semantics of Concurrent Languages in the SMoLCS Approach. IBM Journal of Research and Development 31(5), 512–534 (1987)

    Article  MATH  Google Scholar 

  4. Astesiano, E., Reggio, G.: SMoLCS-Driven Concurrent Calculi. In: Ehrig, H., Kowalski, R., Levi, G., Montanari, U. (eds.) CAAP 1987 and TAPSOFT 1987. LNCS, vol. 249, pp. 169–201. Springer, Heidelberg (1987)

    Google Scholar 

  5. Astesiano, E., Reggio, G.: Formalism and Method. T.C.S. 236(1,2), 3–34 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  6. Astesiano, E., Reggio, G.: Labelled Transition Logic: An Outline. Acta Informatica 37(11-12), 831–879 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  7. Astesiano, E., Reggio, G.: Knowledge Structuring and Representation in Requirement Specification. In: Proc. SEKE 2002. ACM Press, New York (2002), Available at ftp://ftp.disi.unige.it/person/ReggioG/AstesianoReggio02a.pdf

    Google Scholar 

  8. Astesiano, E., Reggio, G.: Consistency Issues in Multiview Modelling Techniques. Technical Report DISI–TR–03–05, DISI, Università di Genova, Italy (2003); To appear in Proc. WADT 2002 (2002)

    Google Scholar 

  9. Astesiano, E., Reggio, G.: Tight Structuring for Precise UML-based Requirement Specifications: Complete Version. Technical Report DISI–TR–03–06, DISI, Università di Genova, Italy (2003), Available at ftp://ftp.disi.unige.it/person/ReggioG/ReggioEtAll03c.pdf

  10. Coscia, E., Reggio, G.: JTN: A Java-targeted Graphic Formal Notation for Reactive and Concurrent Systems. In: Finance, J.-P. (ed.) FASE 1999. LNCS, vol. 1577, pp. 77–97. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  11. Damm, W., Harel, D.: LSCs: Breathing Life into Message Sequence Charts. Formal Methods in System Design 19(1), 45–80 (2001)

    Article  MATH  Google Scholar 

  12. Ehrig, H., Mahr, B.: A Decade of TAPSOFT: Aspects of Progress and Prospects in Theory and Practice of Software Development. In: Mosses, P.D., Schwartzbach, M.I., Nielsen, M. (eds.) CAAP 1995, FASE 1995, and TAPSOFT 1995. LNCS, vol. 915, pp. 3–24. Springer, Heidelberg (1995)

    Google Scholar 

  13. Harel, D.: From Play-In Scenarios to Code: An Achievable Dream. IEEE Computer 34(1), 53–60 (2001)

    MathSciNet  Google Scholar 

  14. Hoare, C.A.R.: How did Software Get so Reliable Without Proof? In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol. 1051, pp. 1–17. Springer, Heidelberg (1996)

    Google Scholar 

  15. Jackson, M.: Software Requirements & Specifications: a Lexicon of Practice, Principles and Prejudices. Addison-Wesley, Reading (1995)

    Google Scholar 

  16. Jackson, M.: Problem Frames: Analyzing and Structuring Software Development Problems. Addison-Wesley, Reading (2001)

    Google Scholar 

  17. Jones, C.: Some Mistakes I Have Made and What I Have Learned FromThem. In: Astesiano, E. (ed.) ETAPS 1998 and FASE 1998. LNCS, vol. 1382, p. 7. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  18. OMG Architecture Board MDA Drafting Team. Model Driven Architecture (MDA) (2001), Available at http://cgi.omg.org/docs/ormsc/01-07-01.pdf

  19. Meyer, B.: Object-Oriented Software Construction. Prentice-Hall, Englewood Cliffs (1997)

    MATH  Google Scholar 

  20. Meyer, B.: Software Engineering in the Academy. Computer 34(5), 28–35 (2001)

    Article  Google Scholar 

  21. Minasi, M.: The Software Conspiracy. Mc Graw Hill, New York (2000)

    Google Scholar 

  22. Mosses, P.D.: CoFI: The Common Framework Initiative for Algebraic Specification and Development. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 115–137. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  23. Parnas, D.L.: “Formal Methods” Technology Transfer Will Fail. J. Systems Software 40(3), 195–198 (1998)

    Article  Google Scholar 

  24. Rational. Rational Unified Process© for System Engineering SE 1.0 (2001)

    Google Scholar 

  25. Reggio, G., Astesiano, E.: An Extension of UML for Modelling the non Purely- Reactive Behaviour of Active Objects. Technical Report DISI–TR–00–28, DISI, Università di Genova, Italy (2000), Available at ftp://ftp.disi.unige.it/person/ReggioG/ReggioAstesiano00b.pdf

  26. Reggio, G., Astesiano, E., Choppy, C., Hussmann, H.: Analysing UML Active Classes and Associated State Machines – A Lightweight Formal Approach. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, p. 127. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  27. Reggio, G., Cerioli, M., Astesiano, E.: Towards a Rigorous Semantics of UML Supporting its Multiview Approach. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, p. 171. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  28. Reggio, G., Larosa, M.: A Graphic Notation for Formal Specifications of Dynamic Systems. In: Fitzgerald, J., Jones, C.B. (eds.) FME 1997. LNCS, vol. 1313. Springer, Heidelberg (1997)

    Google Scholar 

  29. UML Revision Task Force. OMG UML Specification 1.3 (1999), Available at http://www.rational.com/media/uml/post.pdf

  30. Wasserman, A.I.: Toward a Discipline of Software Engineering. IEEE Software 13(6), 23–31 (1996)

    Article  Google Scholar 

  31. Wieringa, R.J.: Requirements Engineering: Frameworks for Understanding. John Wiley, Chichester (1996)

    Google Scholar 

  32. Yourdon, E.: Modern Structured Analysis. Prentice-Hall, Englewood Cliffs (1989)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DISI, Università di Genova, Italy

    Egidio Astesiano, Gianna Reggio & Maura Cerioli

Authors
  1. Egidio Astesiano
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gianna Reggio
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Maura Cerioli
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute for Software Technology, Graz University of Technology, Austria

    Bernhard K. Aichernig

  2. Department of Computing and Software, McMaster University, 1280 Main St West, L8S 4K1, Hamilton, ON, Canada

    Tom Maibaum

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Astesiano, E., Reggio, G., Cerioli, M. (2003). From Formal Techniques to Well-Founded Software Development Methods. In: Aichernig, B.K., Maibaum, T. (eds) Formal Methods at the Crossroads. From Panacea to Foundational Support. Lecture Notes in Computer Science, vol 2757. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-40007-3_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-40007-3_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-20527-2

  • Online ISBN: 978-3-540-40007-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation