Loading...
Abstract
This paper describes the implementation of explicit model checking algorithms to verify the nonblocking or nonconflicting property of discrete event systems. Explicit algorithms enumerate and store all reachable states of a synchronous composition. Three alternatives optimised for memory consumption or runtime are described and compared. The algorithms have been implemented in C++ in the discrete event systems library Waters, and experimental results show that they can explore more than 100 million states on standard computers.
Type
Conference Contribution
Type of thesis
Series
Citation
Malik, R. (2016). Programming a fast explicit conflict checker. In Proceeding of the 13th International Workshop on Discrete Event Systems (pp. 438–443). Xi’an China: IEEE. http://doi.org/10.1109/WODES.2016.7497885
Date
2016
Publisher
IEEE
Degree
Supervisors
Rights
This is an author’s accepted version of an article published in the Proceedings of the 13th International Workshop on Discrete Event Systems. ©2016 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.