© 1996 by British Computer Society
| ||||||||||||||||||||||||||||||||||||||||||||||||||||
A Theory of Prioritizing Composition

1 Department of Computer Science, Abo Akademi University, Lemminkaisenkatu 14, 20520 Turku, 2 Department of Computer Science and Applied Mathematics, University of Kuopio, PO Box 6711, 70211 Kuopio, Finland. Email: Emil.Sekerinski{at}abo.fi
An operator for the composition of two processes, where one process has priority over the other process, is studied. Processes are described by action systems, and data refinement is used for transforming processes. The operator is shown to be compositional, i.e. monotonic with respect to refinement. It is argued that this operator is adequate for modelling priorities as found in programming languages and operating systems. Rules for introducing priorities and for raising and lowering priorities of processes are given. Dynamic priorities are modelled with special priority variables which can be freely mixed with other variables and the prioritizing operator in program development. A number of applications show the use of prioritizing composition for modelling and specification in general.
Received June 21, 1996. revised October 22, 1996.
* Department of Computer Science, Åbo Akademi University, Lemminkäisenkatu 14, 20520 Turku
Department of Computer Science and Applied Mathematics, University of Kuopio, PO Box 6711, 70211 Kuopio, Finland Email: Emil.Sekerinski{at}abo.fi