Compositional nonblocking verification with always enabled events and selfloop-only events

Simple item page
dc.contributor.authorPilbrow, Colin
dc.contributor.authorMalik, Robi
dc.contributor.editorArtho, C.
dc.contributor.editorOlveczky, P.C.
dc.coverage.spatialConference held at Queenstown, NZ
dc.date.accessioned2013-11-18T23:19:20Z
dc.date.accessioned2015-02-16T23:11:36Z
dc.date.available2013-10-29
dc.date.available2015-02-16T23:11:36Z
dc.date.issued2013-10-29
dc.description.abstractThis paper proposes to improve compositional nonblocking verification through the use of 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, i.e., in the part of the system not being simplified. 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. 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.identifier.citationPilbrow, C., & Malik, R. (2013). Compositional nonblocking verification with always enabled events and selfloop-only events. In C. Artho & P. C. Olveczky (Eds.), Preliminary Proceedings Second International Workshop on Formal Techniques for Safety-Critical Systems, Queenstown, NZ(pp. 147–162). Springer. http://doi.org/10.1007/978-3-319-05416-2_11en
dc.identifier.doi10.1007/978-3-319-05416-2_11
dc.identifier.urihttps://hdl.handle.net/10289/9201
dc.language.isoenen_NZ
dc.publisherSpringer
dc.relation.isPartOfPreliminary Proceedings Second International Workshop on Formal Techniques for Safety-Critical Systems
dc.relation.replaceshttps://hdl.handle.net/10289/8187
dc.relation.replaces10289/8187
dc.rights© 2013 Springer.en_NZ
dc.sourceFTSCS 2013en_NZ
dc.titleCompositional nonblocking verification with always enabled events and selfloop-only events
dc.typeConference Contribution
pubs.begin-page147
pubs.elements-id23521
pubs.end-page162
pubs.finish-date2013-10-30
pubs.organisational-group/Waikato
pubs.organisational-group/Waikato/FCMS
pubs.organisational-group/Waikato/FCMS/Computer Science
pubs.organisational-group/Waikato/Student
pubs.start-date2013-10-29
pubs.volumeCCIS 419en_NZ
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
ftscs2013.pdf
Size:
172.86 KB
Format:
Adobe Portable Document Format
Description:
Accepted version
Thumbnail Image
Name: ftscs2013.pdf
Size: 172.86 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
Computing and Mathematical Sciences Papers