Model checking of hierarchical state machines

• US 6,324,496 B1
• Filed: 06/18/1998
• Issued: 11/27/2001
• Est. Priority Date: 06/18/1998
• Status: Expired due to Term

• Current Assignee: WSOU Investments, LLC (WSOU Holdings, LLC)
• Original Assignee: Lucent Technologies, Inc. (Nokia Corporation)
• Inventors: Yannakakis, Mihalis, Alur, Rajeev
• Primary Examiner(s): Teska, Kevin J.
• Assistant Examiner(s): PHAN, THAI Q
• Application Number:
  US09/099,372
• Time in Patent Office: 1,258 Days
• Field of Search: 703/2, 703/22, 703/17, 395/500.05, 395/500.06, 714/39, 714/724, 710/130, 702/118, 707/101, 716/4
• US Class Current: 703/17
• CPC Class Codes: G06F 11/3608 using formal methods, e.g. model checking, abstract interpretation theorem proving G06N5/013

Abstract

Model checking is applied to a hierarchical state machine (i.e., a state machine having at least one state (i.e., a superstate) that is itself a state machine) without first flattening the hierarchical state machine. In one embodiment, the model checking involves one or more or reachability, cycle-detection, linear-time requirements, and branching-time requirements analyses. For reachability analysis, in addition to keeping track of whether states have been visited, the algorithm also keeps track of the exit nodes for each superstate. Cycle-detection analysis has two phases: a primary phase in which target states are identified and a secondary phase in which it is determined whether identified target states are part of closed processing paths or loops. For cycle-detection analysis, the algorithm keeps track of (1) whether states have been visited during the primary phase, (2) the exit nodes for each superstate, and (3) whether states have been visited during the secondary phase. For linear-time requirements analysis, a formula is translated into an automaton, and a product construction is defined between the automaton and a hierarchical machine that yields a new hierarchical machine that is then analyzed using the cycle-detection algorithm. For branching-time requirements analysis, a list of subformulas is generated for an original temporal logic formula, where the subformulas are arranged in order of increasing size. An appropriate subroutine is then implemented for each subformula in the list based on the syntax of the subformula. For certain syntaxes, multiple versions are generated of the finite state machine corresponding to each superstate to represent different possible temporal logic conditions, and an appropriate version is selected for the context of each occurrence of the superstate in the hierarchical state machine. After processing the entire list of subformulas, it is determined whether the entry node of the hierarchical state machine satisfies the original temporal logic formula.

Claims

1. A computer-implemented method for testing a hierarchical state machine that models flow of control within a real system, comprising the steps of:

(I) providing the hierarchical state machine for the real system; and

(II) performing model checking on the hierarchical state machine, wherein the real system is a circuit or a computer program and the model checking is applied to the hierarchical state machine without first flattening the hierarchical state machine, wherein the hierarchical state machine is a finite state machine comprising a plurality of states, wherein at least two of the states are multiple instances of a single state machine and the model checking comprises comparison of the hierarchical state machine against at least one correctness requirement to determine whether the hierarchical state machine satisfies the at least one correctness requirement, wherein, during the model checking, each state machine having multiple instances in the hierarchical state machine is analyzed fewer times than its number of instances in the hierarchical state machine using cyclic temporal logic relation.

2. The method of claim 1, wherein the model checking includes a reachability analysis in which reachability of one or more target states is determined while maintaining:

a first set of information to keep track of states that have been visited during the reachability analysis; and

a second set of information to keep track of one or more exit nodes for each state in the hierarchical state machine that is a superstate corresponding to a finite state machine (FSM).

3. The method of claim 2, wherein the reachability analysis is performed by implementing a depth-first-search (DFS) function at the entry node of the hierarchical state machine, wherein the DFS function comprises the following steps applied to a current state:

(a) returning a positive result if the current state is one of the target states;

(b) updating the first set of information to identify the current state as having been visited;

(c) it the current state is a normal state, then, for each state v connected to the current state, if state v has not yet been visited, then implementing the DFS function at state v; and

(d) it the current state is a superstate, then;

(1) if the entry node of the FSM corresponding to the current state has not yet been visited, then implementing the DFS function at the entry node and updating the second set of information to keep track of the one or more exit nodes of the FSM; and

(2) for each state w connected to an exit node of the FSM, if state w has not yet been visited, then implementing the DFS function at state w.

4. The method of claim 1, wherein the model checking includes a cycle-detection analysis in which reachability of one or more target states existing in a closed processing path is determined while maintaining:

a first set of information to keep track of states that have been visited during a first phase of the cycle-detection analysis in which reachability of at least one of the one or more target states is determined;

a second set of information to keep track of one or more exit nodes for each state in the hierarchical state machine that is a superstate corresponding to a finite state machine; and

a third set of information to keep track of states that have been visited during a second phase of the cycle-detection analysis in which it is determined whether a reachable target state is part of a closed processing path.

5. The method of claim 4, wherein the cycle-detection analysis is performed by implementing a primary search function at the entry node of the hierarchical state machine, wherein the primary search function comprises the following steps applied to a current state:

(a) pushing the current state onto a stack;

(b) updating the first set of information to identify the current state as having been visited during a primary search;

(c) if the current state is a normal state, then;

(1) for each state v connected to the current state, if state v has not yet been visited during, a primary search, then implementing the primary search function at state v; and

(2) if the current state is a target state and the current state has not yet been visited during a secondary search, then implementing a second search function at the current state;

(d) if the current state is a superstate, then;

(1) if the entry node of the FSM corresponding to the current state has not yet been visited during a primary search, then implementing the primary search function at the entry node and updating the second set of information to keep track of the one or more exit nodes of the FSM; and

(2) for each exit node u of the FSM;

(i) for each state w connected to exit node u, if state w has not yet been visited during a primary search, then implementing the primary search function at state w;

(ii) if exit node u was visited during a secondary search, then, for each state w connected to exit node u;

(a) if state w is in the stack, then returning a positive result; and

(b) if state w has not yet been visited during a secondary search, then implementing the secondary search function at state w; and

(e) popping the stack, wherein;

the secondary search function comprises the following steps applied to a current state;

(A) updating the third set of information to identify the current state as having been visited during a secondary search; and

(B) if the current state is a normal state, then, for each state v connected to the current state;

(1) if state v is in the stack, then returning a positive result; and

(2) if state v has not yet been visited during a secondary search, then implementing the secondary search function at state v; and

(C) if the current state is a superstate, then, for each state w connected to an exit node of the FSM corresponding to the current state;

(1) if state w is in the stack, then returning a positive result; and

(2) if state w has not yet been visited during a secondary search, then implementing the secondary search function at state w.

6. The method of claim 4, where an automata-emptiness problem is solved using the primary and secondary search functions.

7. The method of claim 4, where a model checking problem for linear temporal logic is solved using the primary and secondary search functions.

8. The invention method of claim 1, wherein the model checking includes a branching-time requirements analysis in which states in the hierarchical state machine are identified that satisfy one or more temporal logic requirements, wherein, for each temporal logic requirement, multiple versions are generated of the FSM corresponding to each state in the hierarchical state machine that is a superstate to represent different possible temporal logic conditions of the FSM and an appropriate FSM version is selected for the context of each occurrence of the superstate in the hierarchical state machine.

9. The invention method of claim 8, wherein the branching-time requirements analysis comprises the following steps applied to the hierarchical state machine for an original temporal logic formula:

(a) generating, from the original temporal logic formula, a list of subformulas arranged in order of increasing size;

(b) for each subformula in the list, implementing a subroutine corresponding to the syntax of the subformula; and

(c) if the entry node of the hierarchical state machine satisfies the original temporal logic formula, then returning a positive result.

10. The method of claim 9, wherein, for a current subformula,

(a) if the current subformula has the syntax of an atomic proposition, then stop;

(b) if the current subformula has the syntax of the logical complement of a formula χ

, then, for each ordinary state u in the hierarchical state machine, if χ

is not satisfied at state u, then indicate that the current subformula is satisfied at state u;

(c) if the current subformula has the syntax of a first formula combined with a second formula by the logical AND operation, then, for each state u in the hierarchical state machine, if the first formula is satisfied at state u and the second formula is satisfied at state u, then indicate that the current subformula is satisfied at state u;

(d) if the current subformula has the syntax that along some path a next state satisfies a formula χ

, then implement a CheckNext subroutine;

(e) if the current subformula has the syntax that along some path a formula χ

is always satisfied, then implement a CheckAlways subroutine; and

(f) if the current subformula has the syntax that a first formula is satisfied along some path until a second formula is satisfied, then implement a CheckUntil subroutine, wherein, during the CheckNext, CheckAlways, and CheckUntil subroutines, for the current subformula, multiple versions are generated of the FSM corresponding to each state in the hierarchical state machine that is a superstate to represent different possible subformula conditions and an appropriate version is selected for the context of each occurrence of the superstate in the hierarchical state machine.

11. The method of claim 1, wherein the real system is a computer program.

12. The method of claim 1, wherein, during the model checking, each state machine having multiple instances in the hierarchical state machine is analyzed only once to achieve model checking having linear time complexity.

13. A machine-readable medium having stored thereon a plurality of instructions, the plurality of instructions including instructions that, when executed by a computer, cause the computer to perform a method for testing a hierarchical state machine that models flow of control within a real system, comprising the steps of:

(I) providing the hierarchical state machine for the real system; and

(II) performing model checking on the hierarchical state machine, wherein the real system is a circuit or a computer program and the model checking is applied to the hierarchical state machine without first flattening the hierarchical state machine, wherein the hierarchical state machine is a finite state machine comprising a plurality of states, wherein at least two of the states are multiple instances of a single state machine and the model checking comprises comparison of the hierarchical state machine against at least one correctness requirement to determine whether the hierarchical state machine satisfies the at least one correctness requirement, wherein, during the model checking, each state machine having multiple instances in the hierarchical state machine is analyzed fewer times than its number of instances in the hierarchical state machine using cyclic temporal logic relation.

14. The medium of claim 13, wherein the model checking includes a reachability analysis in which reachability of one or more target states is determined while maintaining:

a first set of information to keep track of states that have been visited during the reachability analysis; and

a second set of information to keep track of one or more exit nodes for each state in the hierarchical state machine that is a superstate corresponding to a finite state machine (FSM).

15. The medium of claim 14, wherein the reachability analysis is performed by implementing a depth-first-search (DFS) function at the entry node of the hierarchical state machine, wherein the DFS function comprises the following steps applied to a current state:

(a) returning a positive result if the current state is one of the target states;

(b) updating the first set of information to identify the current state as having been visited;

(c) if the current state is a normal state, then, for each state v connected to the current state, if state v has not yet been visited, then implementing the DFS function at state v; and

(d) if the current state is a superstate, then;

(1) if the entry node of the FSM corresponding to the current state has not yet been visited, then implementing the DFS function at the entry node and updating the second set of information to keep track of the one or more exit nodes of the FSM; and

(2) for each state w connected to an exit node of the FSM, if state w has not yet been visited, then implementing the DFS function at state w.

16. The medium of claim 13, wherein the model checking includes a cycle-detection analysis in which reachability of one or more target states existing in a closed processing path is determined while maintaining:

a first set of information to keep track of states that have been visited during a first phase of the cycle-detection analysis in which reachability of at least one of the one or more target states is determined;

a second set of information to keep track of one or more exit nodes for each state in the hierarchical state machine that is a superstate corresponding to a finite state machine; and

a third set of information to keep track of states that have been visited during a second phase of the cycle-detection analysis in which it is determined whether a reachable target state is part of a closed processing path.

17. The medium of claim 16, wherein the cycle-detection analysis is performed by implementing a primary search function at the entry node of the hierarchical state machine, wherein the primary search function comprises the following steps applied to a current state:

(a) pushing the current state onto a stack;

(b) updating the first set of information to identify the current state as having been visited during a primary search;

(c) if the current state is a normal state, then;

(1) for each state v connected to the current state, if state v has not yet been visited during a primary search, then implementing the primary search function at state v; and

(2) if the current state is a target state and the current state has not yet been visited during a secondary search, then implementing a second search function at the current state;

(d) if the current state is a superstate, then;

(1) if the entry node of the FSM corresponding to the current state has not yet been visited during a primary search, then implementing the primary search function at the entry node and updating the second set of information to keep track of the one or more exit nodes of the FSM; and

(2) for each exit node u of the FSM;

(i) for each state w connected to exit node u, if state w has not yet been visited during a primary search, then implementing the primary search function at state w;

(ii) if exit node u was visited during a secondary search, then, for each state w connected lo exit node u;

(a) if state w is in the stack, then returning a positive result; and

(b) if state w has not yet been visited during a secondary search, then implementing the secondary search function at state w; and

(e) popping the stack, wherein;

the secondary search function comprises the following steps applied to a current state;

(A) updating the third set of information to identify the current state as having been visited during a secondary search; and

(B) if the current state is a normal state, then, for each state v connected to the current state;

(1) if state v is in the stack, then returning a positive result; and

(2) if state v has not yet been visited during a secondary search, then implementing the secondary search function at state v; and

(C) if the current state is a superstate, then, for each state w connected to an exit node of the FSM corresponding to the current state;

(1) if state w is in the stack, then returning a positive result; and

(2) if state w has not yet been visited during a secondary search, then implementing the secondary search function at state w.

18. The medium of claim 16, where at least one of an automata-emptiness problem and a model checking problem for linear temporal logic is solved using the primary and secondary search functions.

19. The medium of claim 13, wherein the model checking includes a branching-time requirements analysis in which states in the hierarchical state machine are identified that satisfy one or more temporal logic requirements, wherein, for each temporal logic requirement, multiple versions are generated of the FSM corresponding to each state in the hierarchical state machine that is a superstate to represent different possible temporal logic conditions of the FSM and an appropriate FSM version is selected for the context of each occurrence of the superstate in the hierarchical state machine.

20. The invention medium of claim 19, wherein the branching-time requirements analysis comprises the following steps applied to the hierarchical state machine for an original temporal logic formula:

(a) generating, from the original temporal logic formula, a list of subformulas arranged in order of increasing size;

(b) for each subformula in the list, implementing a subroutine corresponding to the syntax of the subformula; and

(c) if the entry node of the hierarchical state machine satisfies the original temporal logic formula, then returning a positive result.

21. The medium of claim 20, wherein, for a current subformula,

(a) if the current subformula has the syntax of an atomic proposition, then stop;

(b) if the current subformula has the syntax of the logical complement of a formula χ

, then, for each ordinary state u in the hierarchical state machine, if χ

is not satisfied at state u, then indicate that the current subformula is satisfied at state u;

(c) if the current subformula has the syntax of a first formula combined with a second formula by the logical AND operation, then, for each state u in the hierarchical state machine, if the first formula is satisfied at state u and the second formula is satisfied at state u, then indicate that the current subformula is satisfied at state u;

(d) if the current subformula has the syntax that along some path a next state satisfies a formula χ

, then implement a CheckNext subroutine;

(e) if the current subformula has the syntax that along some path a formula χ

is always satisfied, then implement a CheckAlways subroutine, and

(f) if the current subformula has the syntax that a first formula is satisfied along some path until a second formula is satisfied, then implement a CheckUntil subroutine, wherein, during the CheckNext, CheckAlways and CheckUntil subroutines, for the current subformula, multiple versions are generated of the FSM corresponding to each state in the hierarchical state machine that is a superstate to represent different possible subformula conditions and an appropriate version is selected for the context of each occurrence of the superstate in the hierarchical state machine.

22. The medium of claim 13, wherein the real system is a computer program.

23. The method of claim 13, wherein, during the model checking, each state machine having multiple instances in the hierarchical state machine is analyzed only once to achieve model checking having linear time complexity.

24. A computer-implemented method for testing a hierarchical state machine that models flow of control within a real system, wherein the real system is a circuit or a computer program and model checking is applied to the hierarchical state machine without first flattening the hierarchical state machine, wherein the hierarchical state machine is a finite state machine comprising a plurality of states, wherein at least two of the states are multiple instances of a single state machine and the model checking comprises comparison of the hierarchical state machine against at least one correctness requirement to determine whether the hierarchical state machine satisfies the at least one correctness requirement, wherein, during the model checking, each state machine having multiple instances in the hierarchical state machine is analyzed fewer times than its number of instances in the hierarchical state machine using cyclic temporal logic relation.

25. The method of claim 24, wherein, during the model checking, each state machine having multiple instances in the hierarchical state machine is analyzed only once to achieve model checking having linear time complexity.