×

Formal software development in the verification support environment (VSE). (English) Zbl 1010.68026

Summary: A survey of the VSE system, a CASE-tool for formal software development, is presented. Main emphasis is put on the underlying formal method and tool support, and that in particular from the deductive support perspective. In order to demonstrate its broad range of applicability and to give an impression on how to work with the system we make use of two (commercial) applications taken from the safety and the IT-security domain.

MSC:

68N01 General topics in the theory of software
68Q65 Abstract data types; algebraic specification

Software:

Z
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abrial J.-R., Lecture Notes in Computer Science 552 pp 398– (1991)
[2] Astesiano E., Algebraic foundations of systems specification (1999) · Zbl 0973.68002 · doi:10.1007/978-3-642-59851-7
[3] DOI: 10.1007/BFb0095435 · doi:10.1007/BFb0095435
[4] Autexier S., Proceedings Workshop on Algebraic Development Techniques, WADT-99 (2000)
[5] Boyer R. S., A Computational Logic (1979)
[6] DOI: 10.1007/BF01201353 · Zbl 0010.14501 · doi:10.1007/BF01201353
[7] Heisel M., volume 230 of LNCS, in: Proceedings of the 8th International Conference on Automated Deduction pp 131– (1986)
[8] DOI: 10.1023/A:1005772217686 · Zbl 0881.68108 · doi:10.1023/A:1005772217686
[9] Hutter D., Proceedings Automated Software Engineering, ASE-2000 (2000)
[10] Hutter D., Proceedings Formal Methods Europe 1996: Industrial Benefits and Advances in Formal Methods (1996)
[11] DOI: 10.1007/3-540-48257-1_26 · doi:10.1007/3-540-48257-1_26
[12] DOI: 10.1145/177492.177726 · doi:10.1145/177492.177726
[13] DOI: 10.1145/177492.177726 · doi:10.1145/177492.177726
[14] Loeckx J., Specification of Abstract Data Types (1995) · Zbl 0596.68028
[15] Manna Z., The Temporal Logic of Reactive and Concurrent Systems (1991) · Zbl 0753.68003
[16] Nelson T., Creative Computing 6 pp 56– (1980)
[17] Reif W., volume 620 of LNCS, in: Symposium on Logical Foundations of Computer Science (1992)
[18] Rock G., Tool Support for System Specification, Development and Verification, Advances in Computing Science pp 217– (1999) · doi:10.1007/978-3-7091-6355-9_16
[19] Rutkowski C., BYTE 7 pp 291– (1982)
[20] Spivey J. M., The Z Notation: A Reference Manual. Series in Computer Science (1992) · Zbl 0777.68003
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.