Linking Object-Z with Spec#

Qin, S.; He, G.

doi:10.1109/iceccs.2007.27

Linking Object-Z with Spec#

Qin, S.; He, G.

Authors

S. Qin

G. He

Abstract

Formal specifications have been a focus of software engineering research for many years and have been applied in a wide variety of settings. Their use in software engineering not only promotes high-level verification via theorem proving or model checking, but also inspires the "correct-by- construction" approach to software development via formal refinement. Although this correct-by-construction method proves to work well for small software systems, it is still a Utopia in the development of large and complex software systems. This paper moves one step forward in this direction by designing and implementing a sound linkage between the high level specification language Object-Z and the object-oriented specification language Spec#. Such a linkage would allow system requirements to be specified in a high-level formal language but validated and used in program language level. This linking process can be readily integrated with an automated program refinement procedure to achieve correctness-by-construction. In case no such procedures are applicable, the obtained contract- based specification can guide programmers to manually generate program code, which can then be verified against the obtained specification using any available program verifiers.

Citation

Qin, S., & He, G. (2007). Linking Object-Z with Spec#. In 12th IEEE International Conference on Engineering of Complex Computer Systems, 11-14 Jul 2007, Auckland, New Zealand ; proceedings (185-196). https://doi.org/10.1109/iceccs.2007.27

Conference Name	12th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2007)
Conference Location	Auckland, New Zealand
Start Date	Jul 11, 2007
End Date	Jul 14, 2007
Publication Date	Jul 1, 2007
Deposit Date	Nov 17, 2009
Publicly Available Date	Nov 8, 2010
Publisher	Institute of Electrical and Electronics Engineers
Pages	185-196
Book Title	12th IEEE International Conference on Engineering of Complex Computer Systems, 11-14 Jul 2007, Auckland, New Zealand ; proceedings.
DOI	https://doi.org/10.1109/iceccs.2007.27

Files

Published Conference Proceeding (237 Kb)
PDF

Copyright Statement
© 2007 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.