Progress assumption in concurrent systems
José Félix Costa, Amı́lcar Sernadas · Formal Aspects of Computing · 1995
Abstract A denotational semantics and a sound and complete inequational proof systems for processes with varying degrees of liveness is presented. New insights on quiescence are given concerning the Jonsson characterisation of input/output system. A theory of transational behaviour of the type carry out until the end is developed as an application of this concept of process with liveness requirements. The proposed model fully reflects the parallel composition of transactional requirements , giving the expected composite requirements.