Distance-Vector Routing Protocols in mCRL2

Abstract

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.