Saturation Effects in Testing of Formal Models

Formal analysis of software is a powerful analysis tool, but can be too costly. Random search of formal models can reduce that cost, but is theoretically incomplete. However, random search of finite-state machines exhibits an early saturation effect, i.e., random search quickly yields all that can be found, even after a much longer search. Hence, we avoid the theoretical problem of incompleteness, provided that testing continues until after the saturation point. Such a random search is rapid, consumes little memory, is simple to implement, and can handle very large formal models (in one experiment shown here, over 10178 states).

• Type: Conference
• Year: 2002
• Where: ISSRE
• Authors: Tim Menzies, David Owen, Bojan Cukic
• Keywords: Formal Models, ISSRE 2002, Powerful Analysis Tool, Random Search, Software Engineering