Verification of UML state machines
First Claim
Patent Images
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 variableconverting 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.
1 Assignment
0 Petitions
Accused Products
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.
-
Citations
17 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. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9)
-
-
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. - View Dependent Claims (11, 12, 13, 14, 15, 16)
-
-
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.
-
Specification