Abstract
The reliability of complex software systems is becoming increasingly important for the technical systems they are embedded in. In order to assure the highest levels of trustworthiness of software formal methods for the development of software are required. The VSE-tool was developed by a consortium of German universities and industry to make a tool available which supports this formal development process.
VSE is based on a particular method for programming in the large. This method is embodied in an administration system to edit and maintain formal developments. A deduction component is integrated into this administration system in order to provide proof support for the formed concepts.
In parallel to the development of the system itself, two large case studies were conducted in close collaboration with an industrial partner. In both cases components of systems previously developed by the industry were re-developed from scratch, starting with a formal specification derived from the original documents.
This paper focuses on the deduction component and its integration. We use a part of one of the industrial case studies in order to illustrate the important aspects of the deduction component: We argue that a close integration which makes the structure of developments visible for the theorem prover is necessary for an efficient treatment of changes and an indispensable structuring of the deduction process itself. Also we commend an architecture for interactive strategic theorem proving which has turned out to be adequate for applications in the context of formal program development. The last one of the three main sections addresses the important point of detecting bugs in implementations and specifications.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
J.R. Abrial, M.K.O. Lee, D.S. Neilson, P.N. Scharbach, and I.H. Sorensen. The B-method (software development). In W.J. Prehn, S. Toetenel, editor, VDM 91. Formal Software Development Methods. 4th International Symposium of VDM Europe Proceedings., volume 2, pages 398–405. BP Res., Sunbury Res. Centre, Sunbury-on-Thames, UK, Springer-Verlag, Berlin, Germany, October 1991.
P. Baur, E. Canver, J. Cleve, R. Drexler, R. Förster, P. Göhner, H. Hauff, D. Hutter, P. Kejwal, D. Loevenich, W. Reif, C. Sengler, W. Stephan, M. Ullmann, and A. Wolpers. The Verification Support Environment VSE. In Safety of Computer Control Systems 1992 (SAFECOMP'92), 1992.
Susanne Biundo, Birgit Hummel, Dieter Hutter, and Christoph Walther. The Karlsruhe Induction Theorem Proving System. In Jörg H. Siekmann, editor, Proceedings 8 th International Conference on Automated Deduction (CADE), Lecture Notes in Computer Science (LNCS) 230, pages 672–674, Oxford, England, 1986. Springer-Verlag, Berlin, Germany.
R. S. Boyer and J. Strother Moore. A Computational Logic. Academic Press, London, England, 1979.
The B-Toolkit. B-Core(UK) Limited, October 1994.
M.J.C. Gordon and T.F. Melham. Introduction to HOL. Cambridge University Press, 1993.
Maritta Heisel, Wolfgang Reif, and Werner Stephan. Tactical Theorem Proving in Program Verification. In Proceedings of the 10 th International Conference on Automated Deduction, volume 449 of Lecture Notes in Artificial Intelligence (LNAI), pages 115–131. Springer-Verlag, Berlin, Germany, 1990.
Dieter Hutter. Guiding induction proofs. In Mark E. Stickel, editor, Proceedings 10 th International Conference on Automated Deduction (CADE), Lecture Notes in Artificial Intelligence (LNAI) 449, pages 147–161, Kaiserslautern, Germany, July 1990. Springer-Verlag, Berlin, Germany.
IT-Sicherheitskriterien. Bundesanzeiger, 1989.
Cliff B. Jones. Systematic Software Development using VDM. Prentice Hall, 1990.
Leslie Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3), 1994.
V. R. Pratt. Semantical Considerations on Floyd-Hoare Logic. In Proc. 17th IEEE Symp. on Foundations of Computer Science, pages 109–121, October 1976.
Wolfgang Reif. Correctness of Generic Modules. In Nerode and Taitslin, editors, Symposium on Software Technology and Theoretical Computer Science, volume 620 of Lecture Notes in Computer Science (LNCS). Springer-Verlag, Berlin, Germany, 1992. Tver, Russia.
Wolfgang Reif. Verification of Large Software Systems. In Shyamasundar, editor, Foundations of Software Technology and Theoretical Computer Science, volume 652 of LNCS. Springer-Verlag, Berlin, Germany, 1992. New Dehli, India.
J. Rushby, F. von Henke, and S. Owre. An Introduction to Formal Specification and Verification using EHDM. Technical report, SRI International, March 1991.
J. M. Spivey. The Z Notation: A Reference Manual. Series in Computer Science. Prentice Hall International, 2nd edition, 1992.
Sprachbeschreibung VSE-SL, 1994. Version 1.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hutter, D., Langenstein, B., Sengler, C., Siekmann, J.H., Stephan, W., Wolpers, A. (1996). Deduction in the Verification Support Environment (VSE). In: Gaudel, MC., Woodcock, J. (eds) FME'96: Industrial Benefit and Advances in Formal Methods. FME 1996. Lecture Notes in Computer Science, vol 1051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60973-3_92
Download citation
DOI: https://doi.org/10.1007/3-540-60973-3_92
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60973-5
Online ISBN: 978-3-540-49749-3
eBook Packages: Springer Book Archive