Real-time specification and modeling with joint actions

AbstractThe notion of joint actions provides a natural execution model for a specification language, when temporal logic of actions is used for formal reasoning. We extend this basis with scheduling, the role of which is to enforce liveness properties and to introduce real-time properties. This is done in a way that agrees with the partial-order view of computations and can be applied already in the early stages of specification and design. This leads to distinguishing between schedulings that are totally correct, partially correct, or incorrect with respect to liveness properties. A general scheduling policy of durational actions is formulated from which any reasonable scheduling can be obtained by reducing its nondeterminism. When this policy is totally correct for a system and gives the required real-time properties, no special limitations are imposed on the implementation. The approach also leads to a general classification of real-time models according to the permitted interactions between the computational state and real time