Progress Checking for Dummies
Valmari, A., & Hansen, H. (2018). Progress Checking for Dummies. In F. Howar, & J. Barnat (Eds.), FMICS 2018 : Formal Methods for Industrial Critical Systems (pp. 115-130). Springer. Lecture Notes in Computer Science, 11119. https://doi.org/10.1007/978-3-030-00244-2_8
Published in
Lecture Notes in Computer ScienceDate
2018Copyright
© Springer Nature Switzerland AG 2018
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.
Publisher
SpringerParent publication ISBN
978-3-030-00243-5Conference
Formal Methods for Industrial Critical SystemsIs part of publication
FMICS 2018 : Formal Methods for Industrial Critical SystemsISSN Search the Publication Forum
0302-9743Keywords
Publication in research information system
https://converis.jyu.fi/converis/portal/detail/Publication/28240901
Metadata
Show full item recordCollections
License
Related items
Showing items with similar title or keywords.
-
Material, mental, and moral progress : American conceptions of civilization in late 19th century studies on "things Chinese and Japanese"
Pennanen, Henna-Riikka (University of Jyväskylä, 2015) -
Visions of a technological future : experience and expectation of progress in the interwar United States
Alanko, Antti (2015)Tarkastelen tutkielmassa maailmansotien välisenä aikana Yhdysvaltalaisissa tiede- ja tekniikkajulkaisuissa Popular Mechanicsissa ja Popular Science Monthlyssa esiintynyttä tulevaisuusajattelua. Tutkielman tarkoituksena on ... -
Curiously Empty Intersection of Proof Engineering and Computational Sciences
Kiiskinen, Sampsa (Springer, 2023)The tools and techniques of proof engineering have not yet been applied to the computational sciences. We try to explain why and investigate their potential to advance the field. More concretely, we formalize elementary ... -
Mutation testing in functional programming
Hopia, Tuomo (2023)In software engineering, mutation testing is a method to assess and improve software test quality. It is more prevalent in object-oriented programming and has only seen little interest in functional programming. In this ... -
Students’ approaches to solving R-FCI tasks observed by eye-tracking method
Kekule, Martina; Viiri, Jouni (Charles University in Prague, Faculty of Education, 2018)This study sought to assess the representational format of task options in the representational variant of the force concept Inventory (R-FCI) test, namely its impact on students’ problem-solving approaches. This was ...