Patent ID: 6408262
Filing Date: 2002-06-18
Classification: G06F

Abstract:
A computer-implemented method of performing a reachability check of a state based system model comprising a set of machines (MI, . . .Mn), said machines each comprising at least one possible state (pSIMi, . . . ,pSkMi), each machine being in one of its comprised states at any given time, the dynamic behavior of said machines (MI, . . . ,Mn) being defined by predefined transitions between said states of each machine (MI, . . . ,Mn) and dependencies (D) between said machines (MI, . . . ,Mn), comprising:an initial set of at least one machine state (F) of said machine (MI, . . . ,Mn); initiating a goal set of machine states (A) representing a condition on states of a subset of machines (MI); and repeating the following steps until the analyzing has terminated positively and/or if the subset of machines (MI) comprises all of said machines (MI, . . . ,Mn): expanding the goal set (A) with a set of states which, via transitions, can be brought into the previous goal set (A) independently of machines not included in (MI), if (A) comprises at least one of the machine states in the initial set of states (F) then terminating positively; and otherwise expanding the subset of machines (MI) with at least a subset of the machines (MI, . . . ,Mn); and indicating the results of the reachability check to a user to allow the user to verify whether or not reachability can be achieved.