Partial unfolding for compositional nonblocking verification of extended finite-state machines

Simple item page
dc.contributor.authorMohajerani, Sahar
dc.contributor.authorMalik, Robi
dc.contributor.authorFabian, Martin
dc.date.accessioned2013-02-03T21:05:22Z
dc.date.available2013-02-03T21:05:22Z
dc.date.issued2013-01-30
dc.description.abstractThis working paper describes a framework for compositional nonblocking verification of reactive systems modelled as extended finite-state machines. The nonblocking property can capture the absence of livelocks and deadlocks in concurrent systems. Compositional verification is shown in previous work to be effective to verify this property for large discrete event systems. Here, these results are applied to extended finite-state machines communicating via shared memory. The model to be verified is composed gradually, simplifying components through abstraction at each step, while conflict equivalence guarantees that the final verification 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 verification to achieve substantial state-space reduction.en_NZ
dc.format.mimetypeapplication/pdf
dc.identifier.citationMohajerani, 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.en_NZ
dc.identifier.issn1177-777X
dc.identifier.urihttps://hdl.handle.net/10289/7140
dc.language.isoen
dc.publisherUniversity of Waikato, Department of Computer Scienceen_NZ
dc.relation.ispartofseriesComputer Science Working Papers
dc.rights© 2013 Sahar Mohajerani, Robi Malik, Martin Fabianen_NZ
dc.titlePartial unfolding for compositional nonblocking verification of extended finite-state machinesen_NZ
dc.typeWorking Paperen_NZ
uow.relation.series01/2013
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
uow-cs-wp-2013-01.pdf
Size:
288.51 KB
Format:
Adobe Portable Document Format
Thumbnail Image
Name: uow-cs-wp-2013-01.pdf
Size: 288.51 KB
Kind: Adobe PDF
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.71 KB
Format:
Item-specific license agreed upon to submission
Description:
Name: license.txt
Size: 1.71 KB
Kind: License
Collections
2013 Working Papers