Model Checking of Unrestricted Hierarchical State Machines

Michael Benedikt, Patrice Godefroid, and Thomas Reps

Hierarchical State Machines (HSMs) are a natural model for representing the behavior of software systems. In this paper, we investigate a variety of model-checking problems for an extension of HSMs in which state machines are allowed to call each other recursively.

(Click here to access the paper: PostScript, PDF.)