Heuristic Search for Unbounded Executions
Source: University of Konstanz
The authors present a heuristic search based approach to finding un-bounded executions in software models that can be described using Communicating Finite State Machines (CFSMs). This improves the unboundedness test devised by Jeron and Jard in case certain knowledge about potential sources of unboundedness is available. Such knowledge can be obtained from a boundedness analysis that they designed in precursory work. They evaluate the effectiveness of several different heuristics and search strategies. To show the feasibility of their approach, they compare the performance of the heuristic search algorithms with that of uninformed search algorithms in detecting unbounded executions for a number of case studies.