Graded CTL Model Checking for Test Generation

TL;DR

This paper introduces an efficient graded CTL model-checking algorithm for Hierarchical Finite State Machines, enhancing test generation by providing more counterexamples for better automatic test case creation.

Contribution

It presents a novel model-checking algorithm for graded temporal logics applied to hierarchical models, improving test generation efficiency.

Findings

More counterexamples per run improve test case generation.

Effective verification of HSM models against temporal properties.

Enhanced model-checking performance for hierarchical systems.

Abstract

Recently there has been a great attention from the scientific community towards the use of the model-checking technique as a tool for test generation in the simulation field. This paper aims to provide a useful mean to get more insights along these lines. By applying recent results in the field of graded temporal logics, we present a new efficient model-checking algorithm for Hierarchical Finite State Machines (HSM), a well established symbolism long and widely used for representing hierarchical models of discrete systems. Performing model-checking against specifications expressed using graded temporal logics has the peculiarity of returning more counterexamples within a unique run. We think that this can greatly improve the efficacy of automatically getting test cases. In particular we verify two different models of HSM against branching time temporal properties.