Model checking is an effective way to design correct software. Making behavioural models of software, formulating correctness properties using modal formulas, and verifying these using finite state analysis techniques, is a very efficient way to obtain the required insight in the software. We illustrate this on four common but tricky examples.
CITATION STYLE
Groote, J. F., Keiren, J. J. A., Luttik, B., de Vink, E. P., & Willemse, T. A. C. (2020). Modelling and Analysing Software in mCRL2. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12018 LNCS, pp. 25–48). Springer. https://doi.org/10.1007/978-3-030-40914-2_2
Mendeley helps you to discover research relevant for your work.