A Refinement Strategy for <i>Circus</i>

Formal Aspects of Computing - Tập 15 Số 2-3 - Trang 146-181 - 2003
Ana Cavalcanti1, Augusto Sampaio2, Jim Woodcock1
1Computing Laboratory, University of Kent at Canterbury, CT2 7NF, Canterbury, UK
2Centro de Informática, Universidade Federal de Pernambuco, Recife, PE, Brazil

Tóm tắt

Abstract

We present a refinement strategy for Circus , which is the combination of Z, CSP, and the refinement calculus in the setting of Hoare and He’s unifying theories of programming. The strategy unifies the theories of refinement for processes and their constituent actions, and provides a coherent technique for the stepwise refinement of concurrent and distributed programs involving rich data structures. This kind of development is carried out using Circus ’s refinement calculus, and we describe some of its laws for the simultaneous refinement of state and control behaviour, including the splitting of a process into parallel subcomponents. We illustrate the strategy and the laws using a case study that shows the complete development of a small distributed program.

Từ khóa


Tài liệu tham khảo

Back R. J. R., 1990, [But96] Butler, M.: Stepwise refinement of communicating systems, Science of Computer Programming, 27, 139

Theoretical Computer Science, 2002, Invited paper. [CaW99] Cavalcanti, A. L. C. and Woodcock, J. C. P.: ZRC-A Refinement Calculus for Z. Formal Aspects of Computing, 10, 267

Cavalcanti A. L. C., Proceedings of the Communicating

Processing Architectures, 2002, ZUM'98: The Z

Universitat Oldenburg Fowler, 1999, Refactoring

University Press, 1993, [Hoa72] Hoare, Acta Informatica, 1, 271

European, 1986, Symposium on Programming, 213

1991, International Conference on Concurrency Theory, 61

FME 2002: Formal Methods: Getting IT Right, 2391

Springer-Verlag 2002. [SmD01] Smith G. and Derrick J.: Specification refinement and verification of concurrent systems: An integration of Object-Z and

Systems Design May, 2001, Prentice-Hall, 1992. [Toe92] Toetenel, W. J.: VDM + CCS + Time = MOSCA. In: Proceedings of the IFIP/IFAC Workshop on Real-time Programming

Computing Laboratory 2001. [WoC02] Woodcock J. C. P. and Cavalcanti A. L. C.: The Semantics of Circus. In: Bert D. Bowen J. P. Henson M. C. and Robinson K.

ZB 2002: Formal Specification and Development in Z and B

Springer-Verlag Woodcock, 1996, Using Z: Specification, Refinement, and Proof

1990, editors

Thông tin
Thông tin xuất bản

Formal Aspects of Computing

Tập 15 Số 2-3

146-181

Thông tin tác giả