dc.contributor.author | Valmari, Antti | |
dc.contributor.author | Hansen, Henri | |
dc.contributor.editor | Howar, Falk | |
dc.contributor.editor | Barnat, Jiří | |
dc.date.accessioned | 2018-11-06T13:08:14Z | |
dc.date.available | 2019-09-01T21:35:30Z | |
dc.date.issued | 2018 | |
dc.identifier.citation | Valmari, A., & Hansen, H. (2018). Progress Checking for Dummies. In F. Howar, & J. Barnat (Eds.), <i>FMICS 2018 : Formal Methods for Industrial Critical Systems</i> (pp. 115-130). Springer. Lecture Notes in Computer Science, 11119. <a href="https://doi.org/10.1007/978-3-030-00244-2_8" target="_blank">https://doi.org/10.1007/978-3-030-00244-2_8</a> | |
dc.identifier.other | CONVID_28240901 | |
dc.identifier.other | TUTKAID_78694 | |
dc.identifier.uri | https://jyx.jyu.fi/handle/123456789/60128 | |
dc.description.abstract | Verification of progress properties is both conceptually and
technically significantly more difficult than verification of safety and
deadlock properties. In this study we focus on the conceptual side. We
make a simple modification to a well-known model to demonstrate that
it passes progress verification although the resulting model is intuitively
badly incorrect. Then we point out that the error can be caught easily
by adding a termination branch to the system. We compare the use of
termination branches to the established method of addressing the same
need, that is, weak fairness. Then we discuss another problem that may
cause failure of catching progress errors even with weak fairness. Finally
we point out an alternative notion of progress that needs no explicit fairness
assumptions. Our ideas are especially well-suited for newcomers in
model checking, and work well with stubborn set methods. | fi |
dc.format.mimetype | application/pdf | |
dc.language.iso | eng | |
dc.publisher | Springer | |
dc.relation.ispartof | FMICS 2018 : Formal Methods for Industrial Critical Systems | |
dc.relation.ispartofseries | Lecture Notes in Computer Science | |
dc.rights | In Copyright | |
dc.subject.other | usability of verification methods | |
dc.subject.other | fairness | |
dc.subject.other | fair testing | |
dc.title | Progress Checking for Dummies | |
dc.type | conferenceObject | |
dc.identifier.urn | URN:NBN:fi:jyu-201811064632 | |
dc.contributor.laitos | Informaatioteknologian tiedekunta | fi |
dc.contributor.laitos | Faculty of Information Technology | en |
dc.contributor.oppiaine | Tietojenkäsittelytiede | fi |
dc.contributor.oppiaine | Computer Science | en |
dc.type.uri | http://purl.org/eprint/type/ConferencePaper | |
dc.date.updated | 2018-11-06T07:15:13Z | |
dc.relation.isbn | 978-3-030-00243-5 | |
dc.description.reviewstatus | peerReviewed | |
dc.format.pagerange | 115-130 | |
dc.relation.issn | 0302-9743 | |
dc.relation.numberinseries | 11119 | |
dc.type.version | acceptedVersion | |
dc.rights.copyright | © Springer Nature Switzerland AG 2018 | |
dc.rights.accesslevel | openAccess | fi |
dc.relation.conference | Formal Methods for Industrial Critical Systems | |
dc.subject.yso | ohjelmointi | |
dc.subject.yso | algoritmiikka | |
dc.subject.yso | verifiointi | |
dc.subject.yso | testaus | |
dc.subject.yso | edistys | |
dc.format.content | fulltext | |
jyx.subject.uri | http://www.yso.fi/onto/yso/p4887 | |
jyx.subject.uri | http://www.yso.fi/onto/yso/p3365 | |
jyx.subject.uri | http://www.yso.fi/onto/yso/p6609 | |
jyx.subject.uri | http://www.yso.fi/onto/yso/p8471 | |
jyx.subject.uri | http://www.yso.fi/onto/yso/p8957 | |
dc.rights.url | http://rightsstatements.org/page/InC/1.0/?language=en | |
dc.relation.doi | 10.1007/978-3-030-00244-2_8 | |