An execution model for LOTOS specifications

A model for executing LOTOS (language of temporal ordering specification) specifications (temporal control part) is described. It is based on an activity tree with attributes. The activity tree reflects the dynamic relations between the process invocations and activations of behavior expressions in the specified system, while functions related to the attributes control the execution of interactions and the growing and updating of the tree. The problem of infinite branching, which is caused by non-well-guarded specifications or specifications containing generalized choices, is discussed based on the strategies for growing the activity tree. The general execution model described can also be used as a basis for designing LOTOS implementaton strategies for distributed environments or for systems with parallel processors