A Semantic Model for UNITY
Zhiming Liu · Warwick Research Archive Portal (University of Warwick) · 1989
This paper develops a semantic model for UNITY that reflects its particular aspects, such as nondeterminism, absence of control flow etc. The proposed model is a kind of state-transition system within which observations and actions are the basic semantic objects. An alternative semantics for UNITY programs based on different fairness conditions is also defined using this model. Specially, the fairness condition assumed in [CM88] is defined and the UNITY logic based on it is modelled to show how the safety and liveness (progress) properties can be represented. This model is beeing used as the basis for developing some formal techniques for fault-tolerance within a UNITY framework.