START Conference Manager    

Graded CTL Model Checking for Test Generation

Mimmo Parente and Margherita Napoli

Symposium On Theory of Modeling and Simulation - DEVS Integrative M&S Symposium (TMS/DEVS 2011)
Boston, MA, USA, April 4-9, 2011


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.

START Conference Manager (V2.56.8 - Rev. 1568)