Software Engineering Conference, Australian (2009)
Gold Coast, Australia
Apr. 14, 2009 to Apr. 17, 2009
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ASWEC.2009.12
In this paper we develop an approach for deriving concurrent programs. At any stage in its derivation, a program consists of a combination of the code for its processes together with a set of enforced properties. The behaviour of such a combination consists of those behaviours of the code that satisfy the enforced properties. Because enforced properties are temporal formulae, they may be used to enforce both safety and progress properties of the program. While the code by itself is executable, when combined with enforced properties, the program is not yet in an executable form. A derivation starts from a program in which the desired properties of the code are expressed via enforced properties, and the goal is to derive a program with additional code but no enforced properties. We outline a trace-based theory which formalises the meaning of programs with enforced properties, and transformation rules that ensure each modified program is a refinement of the original.
refinement, concurrency, progress, program derivation, enforced properties
B. Dongol and I. J. Hayes, "Enforcing Safety and Progress Properties: An Approach to Concurrent Program Derivation," 2009 Australian Software Engineering Conference (ASWEC 2009)(ASWEC), Gold Coast, QLD, 2009, pp. 3-12.