Näytä suppeat kuvailutiedot

dc.contributor.authorValmari, Antti
dc.contributor.authorHansen, Henri
dc.contributor.editorHowar, Falk
dc.contributor.editorBarnat, Jiří
dc.date.accessioned2018-11-06T13:08:14Z
dc.date.available2019-09-01T21:35:30Z
dc.date.issued2018
dc.identifier.citationValmari, 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.otherCONVID_28240901
dc.identifier.otherTUTKAID_78694
dc.identifier.urihttps://jyx.jyu.fi/handle/123456789/60128
dc.description.abstractVerification 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.mimetypeapplication/pdf
dc.language.isoeng
dc.publisherSpringer
dc.relation.ispartofFMICS 2018 : Formal Methods for Industrial Critical Systems
dc.relation.ispartofseriesLecture Notes in Computer Science
dc.rightsIn Copyright
dc.subject.otherusability of verification methods
dc.subject.otherfairness
dc.subject.otherfair testing
dc.titleProgress Checking for Dummies
dc.typeconferenceObject
dc.identifier.urnURN:NBN:fi:jyu-201811064632
dc.contributor.laitosInformaatioteknologian tiedekuntafi
dc.contributor.laitosFaculty of Information Technologyen
dc.contributor.oppiaineTietojenkäsittelytiedefi
dc.contributor.oppiaineComputer Scienceen
dc.type.urihttp://purl.org/eprint/type/ConferencePaper
dc.date.updated2018-11-06T07:15:13Z
dc.relation.isbn978-3-030-00243-5
dc.description.reviewstatuspeerReviewed
dc.format.pagerange115-130
dc.relation.issn0302-9743
dc.relation.numberinseries11119
dc.type.versionacceptedVersion
dc.rights.copyright© Springer Nature Switzerland AG 2018
dc.rights.accesslevelopenAccessfi
dc.relation.conferenceFormal Methods for Industrial Critical Systems
dc.subject.ysoohjelmointi
dc.subject.ysoalgoritmiikka
dc.subject.ysoverifiointi
dc.subject.ysotestaus
dc.subject.ysoedistys
dc.format.contentfulltext
jyx.subject.urihttp://www.yso.fi/onto/yso/p4887
jyx.subject.urihttp://www.yso.fi/onto/yso/p3365
jyx.subject.urihttp://www.yso.fi/onto/yso/p6609
jyx.subject.urihttp://www.yso.fi/onto/yso/p8471
jyx.subject.urihttp://www.yso.fi/onto/yso/p8957
dc.rights.urlhttp://rightsstatements.org/page/InC/1.0/?language=en
dc.relation.doi10.1007/978-3-030-00244-2_8


Aineistoon kuuluvat tiedostot

Thumbnail

Aineisto kuuluu seuraaviin kokoelmiin

Näytä suppeat kuvailutiedot

In Copyright
Ellei muuten mainita, aineiston lisenssi on In Copyright