Abstract
Tool support is an essential requirement for the applicability of Formal Methods to realistic, large-scale systems, and the acceptance of Formal Methods in industries in general. Many examples demonstrate how useful the currently existing tools can be especially during the specification and design phase. Essential prerequisites are modularity and scalability of the underlying method. Due to the availability of mature methods and related tools the interest of the Formal Methods community has shifted from the development of new methods to linking of theories and the combination of tools. In this paper an example for the combined use of existing tools is presented, namely the verification condition generator PAMELA (see Buth (1995)) and the proof checker PVS (see Crow et.al.(1995)).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bjørner D., Hoare, C. A. R., Bowen, J., He, J., Langmaack, H., Olderog, E.-R., Martin, U., Stravridou, V., Nielson, F., Nielson, 11.-R., Barringer, H., Edwards, D., LOvengreen, 11.-H., Ravn, A. P., and Rischel, H. (1989): A ProCoS project description–ESPRIT BRA 3014. Bulletin of the EATCS 39, 60–73.
Buth, B., Buth, K.H., Martin, U., and Stavridou, V. (1989): Experiments with program verification systems. ProCoS Technical Report Kiel BB2, Christian-Albrechts-Universität Kiel.
Buth, B. (1995): Operation Refinement Proofs for VDM-like Specifications, Dissertation; published as Technical Report 9501 Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel. (see also: http://www.informatik.uni-bremen.de/~bb)
Buth, B. (1998): An Interface between PAMELA and PVS, Report, in preparation. Buth, B., Cardell-Oliver, R., and Peleska, J. (1998): Combining Tools for the Verification of Fault-Tolerant Systems. In: Tools for System Development and Verification, (Workshop Proceedings), BISS Monographs, Shaker, 1998.
Crow,J., Owre,S., Rushby, J., Shankar,S., and Srivas,M. (1995): A Tutorial Introduction to PVS, Presented at WIFT ‘85: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida; (see also: http://www.csl.sri.com/wift-tutorial.html)
de Bakker, J.-W. (1980): Mathematical Theory of Program Correctness. Series in Computer Science. Prentice-Hall International.
Hoare, C.A.R. (1985): Communicating Sequential Processes; Prentice Hall International.
Jones, C.B. (1990): Systematic Software Development using VDM, Series in Computer Science. Prentice-Hall International, Second Edition.
Heisel, M., Reif, W., and Stephan, W. (1990) Tactical theorem proving in program verification. in Stickel, M. E. (ed.) Proceedings of the 10th International Conference on Automated Deduction, Kaiserslautern, FRG, LNAI 449, pp 117–131. Springer-Verlag.
Peleska, J. and Siegel, M. (1996): Test Automation of Safety-Critical Reactive Systems. South African Computer Jounal (1997) 19: 53–77. Also available as Bericht Nr. 9614, Dezember 1996, Institut für Informatik und praktische Mathematik, Christian¬Albrechts-Universität Kiel.
Peleska, J. (1996): Formal Methods and the Development of Dependable Systems; Habil itationsschrift, Technical Report 9612, Institut für Informatik, Christian-Albrechts Universität Kiel; (see also: http://www. informatik.uni-bremen.de/jp)
The RAISE Method Group (1995): The RAISE Development Method. The Practitioner Series, Prentice Hall.
Weber-Wulff, D. (1993): Proof movie - a proof with the Boyer-Moore Prover. in:Forrnal Aspects of Computing 5(2), 121–151.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Wien
About this paper
Cite this paper
Buth, B. (1999). PAMELA+PVS Verification of Sequential Programs. In: Berghammer, R., Lakhnech, Y. (eds) Tool Support for System Specification, Development and Verification. Advances in Computing Science. Springer, Vienna. https://doi.org/10.1007/978-3-7091-6355-9_5
Download citation
DOI: https://doi.org/10.1007/978-3-7091-6355-9_5
Publisher Name: Springer, Vienna
Print ISBN: 978-3-211-83282-0
Online ISBN: 978-3-7091-6355-9
eBook Packages: Springer Book Archive