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.
References
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.
M. Broy and S. Jähnichen, editors. KORSO: Methods, Languages, and Tools to Construct Correct Software. LNCS. Springer Verlag, 1995. to appear.
CIP System Group. The Munich Project CIP. Volume II: The Program Transformation System CIP-S. LNCS 292. Springer-Verlag, 1987.
J. Conclin and M. Begeman. gIBIS: a hypertext tool for exploratory policy discussion. ACM Transactions on Office Informations Systems, 6:303–331, October 1988.
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.
N. Dershowitz. The Evolution of Programs. Birkhäuser, Boston, 1983.
M. Fröhlich and M. Werner. daVinci V1.3 User Manual. Technical report, Universität Bremen, 1994.
R. Goldblatt. Axiomatising the Logic of Computer Programming. LNCS 130. Springer-Verlag, 1982.
D. Gries. The Science of Programming. Springer-Verlag, 1981.
M. Heisel. A formal notion of strategy for software development. Technical Report 94-28, TU Berlin, 1994.
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.
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.
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.
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.
R. Milner. Logic for computable functions: description of a machine implementation. SIGPLAN Notices, 7:1–6, 1972.
L. Osterweil. Software processes are software too. In 9th International Conference on Software Engineering, pages 2–13. IEEE Computer Society Press, 1987.
J. K. Ousterhout. Tcl and the Tk Toolkit. Addison-Wesley, 1994.
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.
C. Potts. A generic model for representing design methods. In International Conference on Software Engineering, pages 217–226. IEEE Computer Society Press, 1989.
C. Rich and R. C. Waters. The programmer's apprentice: A research overview. IEEE Computer, pages 10–25, November 1988.
T. Shepard, S. Sibbald, and C. Wortley. A visual software process language. Communications of the ACM, 35(4):37–44, April 1992.
D. R. Smith. Top-down synthesis of divide-and-conquer algorithms. Artificial Intelligence, 27:43–96, 1985.
D. R. Smith. KIDS: A semi-automatic program development system. IEEE Transactions on Software Engineering, 16(9): 1024–1043, September 1990.
J. Souquières. Aide au Développement de Specifications. Thèse d'Etat, Université de Nancy I, 1993.
J. Souquières and N. Lévy. Description of specification developments. In Proc. of Requirements Engineering '93, pages 216–223, 1993.
D. S. Wile. Program developments: Formal explanations of implementations. Communications of the ACM, 26(11):902–911, November 1983.
Author information
Authors and Affiliations
Editor information
Rights 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