Linking Object-Z with Spec#

Qin, S.; He, G.

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, July). Linking Object-Z with Spec#. Presented at 12th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2007), Auckland, New Zealand

• Presentation Conference Type: Conference Paper (published)
• Conference Name: 12th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2007)
• 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
• Public URL: https://durham-repository.worktribe.com/output/1161600