Loading...
Thumbnail Image
Publication

Compositional nonblocking verificationusing generalised nonblocking abstractions

Abstract
This paper proposes a method for compositional verification of the standard and generalized nonblocking properties of large discrete event systems. The method is efficient as it avoids the explicit construction of the complete state space by considering and simplifying individual subsystems before they are composed further. Simplification is done using a set of abstraction rules preserving generalized nonblocking equivalence, which are shown to be correct and computationally feasible. Experimental results demonstrate the suitability of the method to verify several large-scale discrete event systems models both for standard and generalized nonblocking.
Type
Journal Article
Type of thesis
Series
Citation
Malik, R. & Leduc, R. (2013). Compositional nonblocking verificationusing generalised nonblocking abstractions. IEEE Transactions on Automatic Control, 58 (8), 1-13.
Date
2013
Publisher
IEEE
Degree
Supervisors
Rights
©2013 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.