Performance Evaluation of Specification Types in NuSMV
O. Mirea (TU Delft - Electrical Engineering, Mathematics and Computer Science)
B.P. Ahrens – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
A. Lukina – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
T.J. Coopmans – Graduation committee member (TU Delft - QCD/Coopmans Group)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Systems are becoming increasingly complex and traditional software testing and manual proofs cannot keep up to ensure correctness. Model checking is a method of performing formal verification of a model by exhaustively checking the state-space. NuSMV is a widely used symbolic verifier and supports three different specification languages: computational tree logic (CTL), linear temporal logic (LTL), and property specification language (PSL). While previous benchmarks on NuSMV exist, they do not detail impacts of the specification language on performance. This paper investigates when each type of logic is most suitable. We evaluate three use cases and develop specifications for them, equivalent in all languages. We analyze runtime, memory and size of the internal representation. Our results show CTL is often faster than LTL and PSL, but memory usage varies by model. CTL performs better on simple global properties or those containing 'next' or 'until' operators. In contrast, LTL and PSL perform better on nested 'global' and 'eventually' operators. LTL and PSL perform nearly identically in all metrics. Bounded Model Checking (BMC) generally outperforms Binary Decision Diagrams-based verification, however, due to the bound, BMC does not guarantee global safety.