Skip to main content

Tool support for formal software development: A generic architecture

  • Conference paper
  • First Online:

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

Abstract

We present a formalism independent approach to the design of tools supporting the application of formal methods in software development. It consists of a concept to represent problem solving knowledge, called strategy, and a generic architecture showing how to implement tools for strategy-based development. A prototype system for program synthesis demonstrates the practicality of the approach.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. W. Bibel and K. M. Hörnig. LOPS — a system based on a strategical approach to program synthesis. In A. Biermann, G. Guiho, and Y. Kodratoff, editors, Automatic Program Construction Techniques, pages 69–89. MacMillan, New York, 1984.

    Google Scholar 

  2. M. Broy and S. Jähnichen, editors. KORSO: Methods, Languages, and Tools to Construct Correct Software. LNCS. Springer Verlag, 1995. to appear.

    Google Scholar 

  3. CIP System Group. The Munich Project CIP. Volume II: The Program Transformation System CIP-S. LNCS 292. Springer-Verlag, 1987.

    Google Scholar 

  4. J. Conclin and M. Begeman. gIBIS: a hypertext tool for exploratory policy discussion. ACM Transactions on Office Informations Systems, 6:303–331, October 1988.

    Article  Google Scholar 

  5. D. Craigan, S. Gerhart, and T. Ralston. An international survey of industrial applications of formal methods. Technical Report NISTGCR 93/626, National Institute of Standards and Technology, Computer Systems Laboratory, Gaithersburg, MD 20899, 1993.

    Google Scholar 

  6. N. Dershowitz. The Evolution of Programs. Birkhäuser, Boston, 1983.

    Google Scholar 

  7. M. Fröhlich and M. Werner. daVinci V1.3 User Manual. Technical report, Universität Bremen, 1994.

    Google Scholar 

  8. R. Goldblatt. Axiomatising the Logic of Computer Programming. LNCS 130. Springer-Verlag, 1982.

    Google Scholar 

  9. D. Gries. The Science of Programming. Springer-Verlag, 1981.

    Google Scholar 

  10. M. Heisel. A formal notion of strategy for software development. Technical Report 94-28, TU Berlin, 1994.

    Google Scholar 

  11. M. Heisel, W. Reif, and W. Stephan. Implementing verification strategies in the KIV system. In E. Lusk and R. Overbeek, editors, 9th International Conference on Automated Deduction, LNCS 310, pages 131–140. Springer-Verlag, 1988.

    Google Scholar 

  12. M. Heisel, T. Santen, and D. Zimmermann. A generic system architecture of strategy-based software development. Technical Report 95-8, Technical University of Berlin, 1995.

    Google Scholar 

  13. B. Hoffmann and B. Krieg-Brückner, editors. PROgram Development by SPECification and TRAnsformation, the PROSPECTRA Methodology, Language Family and System. LNCS 680. Springer-Verlag, 1993.

    Google Scholar 

  14. B. Krieg-Brückner, W. Menzel, W. Reif, H. Ruess, T. Santen, D. Schwier, G. Schellhorn, K. Stenzel, and W. Stephan. System Architecture Framework for KORSO. In Broy and Jähnichen [2], 1995. to appear.

    Google Scholar 

  15. R. Milner. Logic for computable functions: description of a machine implementation. SIGPLAN Notices, 7:1–6, 1972.

    Google Scholar 

  16. L. Osterweil. Software processes are software too. In 9th International Conference on Software Engineering, pages 2–13. IEEE Computer Society Press, 1987.

    Google Scholar 

  17. J. K. Ousterhout. Tcl and the Tk Toolkit. Addison-Wesley, 1994.

    Google Scholar 

  18. L. C. Paulson. Isabelle: The next seven hundred theorem provers. In E. Losk and R. Overbeek, editors, Ninth International Conference on Automated Deduction, LNCS 310, pages 772–773. Springer Verlag, 1988.

    Google Scholar 

  19. C. Potts. A generic model for representing design methods. In International Conference on Software Engineering, pages 217–226. IEEE Computer Society Press, 1989.

    Google Scholar 

  20. C. Rich and R. C. Waters. The programmer's apprentice: A research overview. IEEE Computer, pages 10–25, November 1988.

    Google Scholar 

  21. T. Shepard, S. Sibbald, and C. Wortley. A visual software process language. Communications of the ACM, 35(4):37–44, April 1992.

    Article  Google Scholar 

  22. D. R. Smith. Top-down synthesis of divide-and-conquer algorithms. Artificial Intelligence, 27:43–96, 1985.

    Article  MathSciNet  Google Scholar 

  23. D. R. Smith. KIDS: A semi-automatic program development system. IEEE Transactions on Software Engineering, 16(9): 1024–1043, September 1990.

    Article  Google Scholar 

  24. J. Souquières. Aide au Développement de Specifications. Thèse d'Etat, Université de Nancy I, 1993.

    Google Scholar 

  25. J. Souquières and N. Lévy. Description of specification developments. In Proc. of Requirements Engineering '93, pages 216–223, 1993.

    Google Scholar 

  26. D. S. Wile. Program developments: Formal explanations of implementations. Communications of the ACM, 26(11):902–911, November 1983.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Wilhelm Schäfer Pere Botella

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Heisel, M., Santen, T., Zimmermann, D. (1995). Tool support for formal software development: A generic architecture. In: Schäfer, W., Botella, P. (eds) Software Engineering — ESEC '95. ESEC 1995. Lecture Notes in Computer Science, vol 989. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60406-5_20

Download citation

  • DOI: https://doi.org/10.1007/3-540-60406-5_20

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60406-8

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics