Loading...
Thumbnail Image
Item

Seven abstraction rules preserving generalised nonblocking

Abstract
This working paper proposes a compositional approach to verify the generalised nonblocking property of discrete-event systems. Generalised nonblocking is introduced in [15] to overcome weaknesses of the standard nonblocking check in discrete-event systems and increase the scope of liveness properties that can be handled. This paper addresses the question of how generalised nonblocking can be verified efficiently. The explicit construction of the complete state space is avoided by first composing and simplifying individual components in ways that preserve generalised nonblocking. The paper extends and generalises previous results about compositional verification of standard nonblocking and lists a new set of computationally feasible abstraction rules for standard and generalised nonblocking.
Type
Working Paper
Type of thesis
Series
Computer Science Working Papers
Citation
Malik, R. & Leduc, R. (2009). Seven abstraction rules preserving generalised nonblocking. (Working paper 07/2009). Hamilton, New Zealand: University of Waikato, Department of Computer Science.
Date
2009-09-01
Publisher
University of Waikato, Department of Computer Science
Degree
Supervisors
Rights