Verification of UML state machines

• US 9,454,382 B2
• Filed: 10/14/2013
• Issued: 09/27/2016
• Est. Priority Date: 10/14/2013
• Status: Expired due to Fees

• Current Assignee: International Business Machines Corporation
• Original Assignee: International Business Machines Corporation
• Inventors: Adler, Oshri, Razinkov, Natalia, Yorav, Karen
• Primary Examiner(s): Pan, Hang
• Assistant Examiner(s): Lin, Hui-Wen
• Application Number:
  US14/052,777
• Publication Number:
  US 20150106781A1
• Time in Patent Office: 1,079 Days
• Field of Search: 717/104
• US Class Current: 1/1
• CPC Class Codes: G06F 8/35 model driven
• CPC Class Codes: G06F 9/4494 data driven

Abstract

A method, apparatus and computer-implemented method, the method comprising: receiving a statechart comprising a complex feature; and replacing the complex feature with a transformed feature, thereby transforming the statechart to a second statechart, wherein replacing the complex feature comprises: creating an auxiliary variable or a default state; changing a value of the auxiliary variable at the beginning of the transformed feature and changing the value of the auxiliary variable again at its end; and taking a transition from the default state, such that the transition occurs in accordance with the value of the auxiliary variable.

Claims

1. A computer-implemented method performed by a computerized device, comprising:

receiving a statechart comprising at least two complex features; and

for each complex feature of the at least two complex features replacing the complex feature with a transformed feature, thereby transforming the statechart to a second statechart while preserving behavior of the statechart,

wherein replacing the complex feature comprises;

creating an auxiliary variable which was not comprised by the statechart and a default state;

changing a value of the auxiliary variable at the beginning of the transformed feature and changing the value of the auxiliary variable again at its end;

taking a transition from the default state, such that the transition occurs in accordance with the value of the auxiliary variable

converting the second statechart to input format of a verification tool to obtain a model to be verified; and

verifying the model,

wherein the computerized device comprises a processing unit and a storage device.

2. The computer-implemented method of claim 1, wherein the complex feature is a shallow history.

3. The computer-implemented method of claim 1, wherein the complex feature is a fork transition.

4. The computer-implemented method of claim 1, wherein the complex feature is a multilevel transition.

5. The computer-implemented method of claim 1, wherein the complex feature is an exit action of a state.

6. The computer-implemented method of claim 1, wherein the complex feature is an entry action of a state.

7. The computer-implemented method of claim 1, wherein the complex feature is a multi-action transition.

8. The computer-implemented method of claim 1, wherein the complex feature is an IF action.

9. The computer-implemented method of claim 1, wherein the complex feature is a WHILE action.

10. An apparatus comprising:

a processing unit;

a storage device;

an input receiving component for receiving a statechart comprising at least two complex feature; and

a feature elimination component for replacing each complex feature of the at least two complex features with a transformed feature, thereby transforming the statechart to an enhanced statechart while preserving behavior of the statechart,

wherein the feature elimination component comprises commands for;

creating an auxiliary variable which was not comprised by the statechart and a default state;

changing a value of the auxiliary variable at the beginning of the transformed feature and changing the value of the auxiliary variable again at its end;

taking a transition from the default state, such that the transition occurs in accordance with the value of the auxiliary variable

a statechart conversion component for converting the enhanced statechart to input format of a verification toot to obtain a model; and

a model verification component for verifying the model.

11. The apparatus of claim 10, wherein the complex feature is a shallow history.

12. The apparatus of claim 10, wherein the complex feature is a fork transition.

13. The apparatus of claim 10, wherein the complex feature is a multilevel transition.

14. The apparatus of claim 10, wherein the complex feature is an exit action of a state.

15. The apparatus of claim 10, wherein the complex feature is an entry action of a state.

16. The apparatus of claim 10, wherein the complex feature is a multi-action transition.

17. A computer program product comprising:

a non-transitory computer readable medium;

a first program instruction for receiving a statechart comprising at least two complex feature; and

a second program instruction for replacing each complex feature of the at least two complex features with a transformed feature, thereby transforming the statechart to a second statechart while preserving behavior of the statechart,

wherein the second program instruction replacing the complex feature comprises;

a third program instruction for creating an auxiliary variable which was not comprised by the statechart and a default state;

a fourth program instruction for changing a value of the auxiliary variable at the beginning of the transformed feature and changing the value of the auxiliary variable again at its end; and

a fifth program instruction for taking a transition from the default state, such that the transition occurs in accordance with the value of the auxiliary variable,

a sixth program instruction for converting the second statechart to input format of a verification tool to obtain a model to be verified; and

a seventh program instruction for verifying the model,

wherein said first, second, third, fourth, fifth, sixth and seventh program instructions are stored on said non-transitory computer readable medium.