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 inLecture Notes in Computer Science
© 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.
Parent publication ISBN978-3-030-00243-5
ConferenceFormal Methods for Industrial Critical Systems
Is part of publicationFMICS 2018 : Formal Methods for Industrial Critical Systems
Publication in research information system
MetadataShow full item record
Showing items with similar title or keywords.
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 ...
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)
An Approach to the Automatic Comparison of Reference Point-Based Interactive Methods for Multiobjective Optimization Podkopaev, Dmitry; Miettinen, Kaisa; Ojalehto, Vesa (Institute of Electrical and Electronics Engineers (IEEE), 2021)Solving multiobjective optimization problems means finding the best balance among multiple conflicting objectives. This needs preference information from a decision maker who is a domain expert. In interactive methods, the ...
Eronen, Oskari (2005)