State machine method for editing requirements using transition systems, a sub-state mechanism, and a partial behaviors mechanism in order to reduce complexity and the number of states
View Patent ↗A method for providing writing requirements for a structured transition system employing state machines. The requirements employ a plurality of structuring mechanisms, namely, sub-state based structuring, abstraction based structuring and partial behavior structuring that uses event sequences. The sub-state based structuring has to do with the hierarchical requirements of the state machines, abstraction based structuring provides an abstraction of the state machines that reduces the number of states, and partial behavior structuring looks at certain states to predict how those states will affect other states.
1. A method for providing specification requirements for a structured transition system employing state machines, said method performed using a state machine processor, and comprising:
providing a sub-state based structuring mechanism that allows users to focus on the behavior with respect to a sub-set of states;
providing an abstraction based structuring mechanism that allows users to specify requirements by conflating different states;
providing a partial behaviors structuring mechanism that allows specification of transitions using scenarios; and
employing the sub-state based structuring mechanism, the abstraction based structuring mechanism and the partial behaviors structuring mechanism to provide the writing requirements and define syntax and semantics of the system.
2. The method according to claim 1 further comprising providing a decomposition structuring mechanism that operates to reduce the complexity of a large state machine into smaller inter-related state machines, said decomposition structuring mechanism also being employed to provide the writing requirements and define the syntax and semantics of the system.
3. The method according to claim 1 further comprising providing a structured sequence of declarations that define the syntax of the system.
4. The method according to claim 3 wherein the structured sequence of declarations includes type declarations, variable declarations, event declarations, action declarations, invariant declarations, initialization declarations and transition declarations.
5. The method according to claim 3 wherein one of the declarations is a transition declaration including a plurality of syntax elements.
6. The method according to claim 5 wherein the syntax elements include a sub-space syntax element that describes the transition behavior with respect to a set of states using a predicate and an abstraction syntax element that specifies an over-approximation of the behavior of a specification of the system.
7. The method according to claim 5 wherein the transition declaration includes source and target states selected from the group consisting of initial states, state predicates, post image states of a sequence of events and pre-image states of a sequence of events with respect to a given set of states.
8. The method according to claim 1 wherein the state machines are on a vehicle.
9. A method for providing specification requirements for a structured transition system employing state machines on a vehicle, said method performed using a state machine processor, comprising:
providing a sub-state based structuring mechanism that allows users to focus on the behavior with respect to a sub-set of states;
providing an abstraction based structuring mechanism that allows users to specify requirements by conflating different states;
providing a partial behaviors structuring mechanism that allows specification of transition by using scenarios;
providing a decomposition structuring mechanism that allows reducing the complexity of a large state machine into smaller inter-related state machine;
providing a structured sequence of declarations that define the syntax of the system; and
employing the sub-state based structuring mechanism, the abstraction based structuring mechanism, the partial behaviors structuring mechanism and the decomposition structuring mechanism to provide the writing requirements and to define the syntax and semantics of the system.
10. The method according to claim 9 wherein the structured sequence of declarations includes type declarations, variable declarations, event declarations, action declarations, invariant declarations, initialization declarations and transition declarations.
11. The method according to claim 9 wherein one of the declarations is a transition declaration including a plurality of syntax elements.
12. The method according to claim 11 wherein the syntax elements include a sub-space syntax element that describes the transition behavior with respect to a set of states using a predicate and an abstraction syntax element that specifies an over-approximation of the behavior of a specification of the system.
13. The method according to claim 11 wherein the transition declaration includes source and target states selected from the group consisting of initial states, state predicates, post image states of a sequence of events and pre-image states of a sequence of events with respect to a given set of states.
14. A method for providing specification requirements for a structured transition system employing state machines, said method performed using a state machine processor, and comprising:
providing a plurality of structuring mechanisms that reduce the complexity of the state machines and the states employed in the state machines; and
using the plurality of structuring mechanisms to provide the writing requirements and providing syntax and semantics of the system wherein the plurality of structuring mechanisms include a sub-state based structuring mechanism, a partial behaviors structuring mechanism and a decomposition structuring mechanism.
15. The method according to claim 14 further comprising providing a structured sequence of declarations that define the syntax of the system.
16. The method according to claim 15 wherein the structured sequence of declarations includes type declarations, variable declarations, event declarations, action declarations, invariant declarations, initialization declarations and transition declarations.
17. The method according to claim 15 wherein one of the declarations is a transition declaration including a plurality of syntax elements.
18. The method according to claim 17 wherein the syntax elements include a sub-space syntax element that describes the transition behavior with respect to a set of states using a predicate and an abstraction syntax element that specifies an over-approximation of the behavior of a specification of the system.
19. The method according to claim 17 wherein the transition declaration includes source and target states selected from the group consisting of initial states, state predicates, post image states of a sequence of events and pre-image states of a sequence of events with respect to a given set of states.