Partial unfolding for compositional nonblocking verification of extended finite-state machines
Mohajerani, S., Malik, R. & Fabian, M. (2012). Partial unfolding for compositional nonblocking verification of extended finite-state machines. (Working paper 01/2013). Hamilton, New Zealand: University of Waikato, Department of Computer Science.
Permanent Research Commons link: https://hdl.handle.net/10289/7140
This working paper describes a framework for compositional nonblocking veriﬁcation of reactive systems modelled as extended ﬁnite-state machines. The nonblocking property can capture the absence of livelocks and deadlocks in concurrent systems. Compositional veriﬁcation is shown in previous work to be effective to verify this property for large discrete event systems. Here, these results are applied to extended ﬁnite-state machines communicating via shared memory. The model to be veriﬁed is composed gradually, simplifying components through abstraction at each step, while conﬂict equivalence guarantees that the ﬁnal veriﬁcation result is the same as it would have been for the non-abstracted model. The working paper concludes with an example showing the potential of compositional veriﬁcation to achieve substantial state-space reduction.
University of Waikato, Department of Computer Science
© 2013 Sahar Mohajerani, Robi Malik, Martin Fabian
- 2013 Working Papers