An implementation of a compositional approach for verifying generalised nonblocking

Francis, Rachel

An implementation of a compositional approach for verifying generalised nonblocking

dc.contributor.author	Francis, Rachel
dc.date.accessioned	2011-05-04T02:49:11Z
dc.date.available	2011-05-04T02:49:11Z
dc.date.issued	2011-04-27
dc.description.abstract	Generalised nonblocking is a property of discrete-event systems which verifies liveness. It was introduced to overcome the weaknesses of standard nonblocking. Verifying generalised nonblocking of real-world models often involves exploring state-spaces which will exceed available memory. A compositional verification approach has been developed to achieve verification for models of a much larger size. For this project, we have developed the first implementation for compositionally verifying generalised nonblocking. In addition, we have experimented with the techniques used in compositional verification, and analysed their performance. Our algorithm has successfully verified a large set of industrial-size models, including at least one large model which had not been verified before.	en_NZ
dc.format.mimetype	application/pdf
dc.identifier.citation	Francis, R. (2011). An implementation of a compositional approach for verifying generalised nonblocking. (Working paper 04/2011). Hamilton, New Zealand: University of Waikato, Department of Computer Science.	en_NZ
dc.identifier.issn	1177-777X
dc.identifier.uri	https://hdl.handle.net/10289/5312
dc.language.iso	en
dc.publisher	University of Waikato, Department of Computer Science	en_NZ
dc.relation.ispartofseries	Computer Science Working Papers
dc.subject	computer science	en_NZ
dc.title	An implementation of a compositional approach for verifying generalised nonblocking	en_NZ
dc.type	Working Paper	en_NZ
pubs.elements-id	54206
uow.relation.series	04/2011