Show simple item record  

dc.contributor.authorPilbrow, Colinen_NZ
dc.contributor.authorMalik, Robien_NZ
dc.date.accessioned2016-08-10T02:30:32Z
dc.date.available2015-12-01en_NZ
dc.date.available2016-08-10T02:30:32Z
dc.date.issued2015-12-01en_NZ
dc.identifier.citationPilbrow, C., & Malik, R. (2015). An algorithm for compositional nonblocking verification using special events. Science of Computer Programming, 113, 119–148. http://doi.org/10.1016/j.scico.2015.05.010en
dc.identifier.issn0167-6423en_NZ
dc.identifier.urihttps://hdl.handle.net/10289/10586
dc.description.abstractThis paper proposes to improve compositional nonblocking verification of discrete event systems through the use of special 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, i.e., in the part of the system not being simplified. Here, it is proposed to exploit more knowledge about the remainder of the system and check how events are being used. Always enabled events, selfloop-only events, failing events, and blocked events are easy to detect and often help with simplification even though they are used in the remainder of the system. Abstraction rules from previous work are generalised, and experimental results demonstrate the applicability of the resulting algorithm to verify several industrial-scale discrete event system models, while achieving better state-space reduction than before.
dc.format.mimetypeapplication/pdf
dc.language.isoenen_NZ
dc.publisherElsevier Scienceen_NZ
dc.rightsThis is an author’s accepted version of an article published in the journal: Science of Computer Programming. © 2015 Elsevier.
dc.subjectScience & Technologyen_NZ
dc.subjectTechnologyen_NZ
dc.subjectComputer Science, Software Engineeringen_NZ
dc.subjectComputer Scienceen_NZ
dc.subjectDiscrete event systemsen_NZ
dc.subjectFinite-state machinesen_NZ
dc.subjectModel checkingen_NZ
dc.subjectCompositional verificationen_NZ
dc.subjectNonblockingen_NZ
dc.subjectSUPERVISORY CONTROLen_NZ
dc.subjectSYSTEMSen_NZ
dc.subjectEQUIVALENCEen_NZ
dc.subjectFRAMEWORKen_NZ
dc.titleAn algorithm for compositional nonblocking verification using special eventsen_NZ
dc.typeJournal Article
dc.identifier.doi10.1016/j.scico.2015.05.010en_NZ
dc.relation.isPartOfScience of Computer Programmingen_NZ
pubs.begin-page119
pubs.elements-id121281
pubs.end-page148
pubs.publication-statusPublisheden_NZ
pubs.volume113en_NZ
uow.identifier.article-noP2en_NZ


Files in this item

This item appears in the following Collection(s)

Show simple item record