Model checking is a formal verification technique that can be used to ensure correctness of software systems. mCRL2 is a specification language with an accompanying toolset that can perform various operations including model checking. Modal μ-calculus is the property language used by the mCRL2 toolkit. The fixed-point operators included in modal μ-calculus allow it to express inductive properties. These operators give modal μ-calculus very high expressivity, allowing it to encompass other temporal logics such as LTL, CTL, and CTL*. However, this expressivity comes with some downsides as modal μ-calculus formulae can be hard to understand and take more time to verify compared to less expressive logics. In this study we compare the use of fixed-point operators to the use of helper functions for expressing three properties in a case study based on four distance-vector routing protocols. We find that the properties expressed using fixed-point operators were more performant in terms of verification time. We also found that fixed-point operators lead to larger logic expressions but smaller overall expressions when taking the size of the helper functions into account. Furthermore, we conclude that fixed-point operators can be better suited for people experienced with them, while helper functions can be better suited for the average programmer, at least for this type of task.
... Read more