Loading...
Thumbnail Image
Item

Compositional nonblocking verification with always enabled and selfloop-only events

Abstract
This report proposes to improve compositional nonblocking verification through the use of two special event types: always enabled and selfloop-only events. Compositional verification involves abstraction to simplify parts of a system during verification. Normally, this abstraction is based on the set of events not used in the remainder of the system. Here, it is proposed to exploit more knowledge about the system and abstract events even though they are used in the remainder of the system. This can lead to more simplification than was previously possible. Abstraction rules from previous work are extended to respect the new special events and proofs show these rules still preserve nonblocking. The rules have been implemented in Waters and experimental results demonstrate that these extended simplification rules help verify several industrial-scale discrete event system models while achieving better state-space reduction than before.
Type
Working Paper
Type of thesis
Series
Computer Science Working Papers
Citation
Pilbrow, C. (2013). Compositional nonblocking verification with always enabled and selfloop-only events. (Working paper 07/2013). Hamilton, New Zealand: University of Waikato, Department of Computer Science.
Date
2013-11-19
Publisher
University of Waikato, Department of Computer Science
Degree
Supervisors
Rights
© 2013 Colin Pilbrow