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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Dyseryn, V., van Glabbeek, R.J., Höfner, P.: Analysing mutual exclusion using process algebra with signals. In: Peters, K., Tini, S. (eds.) Proceedings of EXPRESS/SOS 2017, Berlin, Germany, 4 September 2017. EPTCS, vol. 255, pp. 18–34 (2017)
Kaivola, R., Valmari, A.: The weakest compositional semantic equivalence preserving nexttime-less linear temporal logic. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 207–221. Springer, Heidelberg (1992). https://doi.org/10.1007/BFb0084793
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer, New York (1992). https://doi.org/10.1007/978-1-4612-0931-7
Pelánek, R.: BEEM: benchmarks for explicit model checkers. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263–267. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73370-6_17
Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115–116 (1981)
Reeves, G.E.: What really happened on Mars? (1997). https://www.cs.unc.edu/%7eanderson/teach/comp790/papers/mars_pathfinder_long_version.html. Accessed 7 May 2018
Rensink, A., Vogler, W.: Fair testing. Inf. Comput. 205(2), 125–198 (2007)
Valmari, A.: The weakest deadlock-preserving congruence. Inf. Process. Lett. 53(6), 341–346 (1995)
Valmari, A.: A chaos-free failures divergences semantics with applications to verification. In: Davies, J., Roscoe, B., Woodcock, J. (eds.) Millennial Perspectives in Computer Science: Proceedings of the 1999 Oxford-Microsoft Symposium in Honour of Sir Tony Hoare, Cornerstones of Computing, pp. 365–382. Palgrave (2000)
Valmari, A., Setälä, M.: Visual verification of safety and liveness. In: Gaudel, M.-C., Woodcock, J. (eds.) FME 1996. LNCS, vol. 1051, pp. 228–247. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-60973-3_90
Valmari, A., Tienari, M.: Compositional failure-based semantics models for basic LOTOS. Formal Asp. Comput. 7(4), 440–468 (1995)
Valmari, A., Vogler, W.: Fair testing and stubborn sets. In: Bošnački, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 225–243. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-32582-8_16
Vogler, W. (ed.): Modular Construction and Partial Order Semantics of Petri Nets. LNCS, vol. 625. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55767-9
Acknowledgements
We thank the anonymous reviewers for their comments.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Valmari, A., Hansen, H. (2018). Progress Checking for Dummies. In: Howar, F., Barnat, J. (eds) Formal Methods for Industrial Critical Systems. FMICS 2018. Lecture Notes in Computer Science(), vol 11119. Springer, Cham. https://doi.org/10.1007/978-3-030-00244-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-030-00244-2_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-00243-5
Online ISBN: 978-3-030-00244-2
eBook Packages: Computer ScienceComputer Science (R0)