2011/11/09 by Margherita Napoli, Napoli, Margherita, Mimmo Parente +1
Computer Science · Engineering · #68Q60 #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Real-time simulation and control systems #Software Testing and Debugging Techniques #cs.FL #cs.LO #msc:68Q60
paper · pdf · doi:10.48550/arxiv.1111.2768
Symposium On Theory of Modeling and Simulation (DEVS/TMS'11)
arxiv created 2011/11/09 · openalex publication_date 2011/11/09 · arxiv updated 2011/11/14 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.