Limitations of Liveness in Concurrent Software Systems

A desirable property of software is that from any reachable state any transition of interest will eventually take place. In this paper, software satisfying this property will be said to be responsive. Responsiveness can be studied on untimed DES models of the software. The paper shows that DES liveness is not sufficient to guarantee that the software will be responsive. Two causes of this problem are identified, namely transition determinism and operation timing. Transition determinism refers to the fact that not any DES enabled transition may be fired, but only the specific transition selected by the software. Operation timing refers to the times at which software execution stages take place. Conditions required to fire a transition may become unlikely or impossible due to operation timing. To address these issues, explicit modeling of deterministic choice is proposed and a special DES structure is introduced. Then, a sufficient condition is formulated under which DES liveness implies software responsiveness. This sufficient condition is then applied to the supervisory control problem in order to identify a class of liveness enforcing supervisors that ensure responsiveness. While Petri nets are used here to represent the DES models, the results are also relevant in the automata framework.