WO2007041901A1

WO2007041901A1 - System and method for formal verification of statecharts

Info

Publication number: WO2007041901A1
Application number: PCT/CN2005/001690
Authority: WO
Inventors: Rui Zhang
Original assignee: Honeywell International, Inc.
Priority date: 2005-10-14
Filing date: 2005-10-14
Publication date: 2007-04-19

Abstract

A system and method formally verifies a statechart. In an embodiment, an UML statechart is translated into an XML-based intermediate language. The XML intermediate language is then translated into a target format, and the target format is verified with a verification tool.

Description

SYSTEM AND METHOD FOR FORMAL VERIFICATION OF STATECHARTS

Technical Field

[0001] The present invention relates to the field of software verification, and in an embodiment, but not by way of limitation, to formal verification of statecharts.

Background

[0002] Formal verification of software systems usually involves building a finite model of a system as a set of states and state transitions and checking that a desired property holds in the model. An exhaustive search of all possible states of the model may be performed in order to verify a desired property.

[0003] Modeling diagrams have become an industry-accepted visual formalism for the modeling of software systems. One popular tool for such modeling diagrams is the Unified Modeling Language (UML), and it is used by software professionals for specifying, visualizing, constructing, and documenting artifacts of software systems. [0004] The UML is an object oriented system, and in its entirety involves nine types of diagrams to model a system. These diagrams types include class, package, object, use case, sequence, collaboration, statechart, activity, component, and deployment. Each diagram type describes a particular part or level of a system. The class diagrams are the backbone of the model. They describe the static structure of the system. Package diagrams are actually a subset of class diagrams, and allow a developer to organize elements of a system into related groups to minimize dependencies between packages. Object diagrams describe the static structure of a system at a particular time, and may be used to test class diagrams for accuracy. Use case diagrams model the functionality of a system using actors and use cases. Sequence diagrams describe interactions among classes in terms of an exchange of messages over time. Collaboration diagrams represent interactions between objects as a series of sequenced messages, and as such, may describe both the static structure and the dynamic behavior of a system. Statechart diagrams describe the dynamic behavior of a system in response to external stimuli. Statechart diagrams are especially useful in modeling reactive objects whose states are triggered by specific events. In many systems, statechart diagrams are a focus of the modeling process, and the software development and modeling community has recently undertaken efforts to verify UML statecharts. Activity diagrams illustrate the dynamic nature of a system by modeling the flow of control from activity to activity. Component diagrams describe the organization of physical software components, including source code, run-time (binary) code, and executables. Lastly, deployment diagrams depict the physical resources in a system, including nodes, components, and connections.

[0005] Several methods exist in the art for verifying UML statecharts. One such method includes translating a UML statechart into the input language format for an existing formal verification tool (such as SMV or SPIN), and then verifying the translation result. However, all of the current solutions that use this approach require a specific source format and a specific target format. Because of this requirement for specific formats, it is very difficult to build a new formal verification system for a source/target format based on existing solutions. With the rapid development of design/modeling tools and formal verification tools (unfortunately, most design tools and formal verification tools are not integrated), a more efficient way to build formal verification systems has become increasingly urgent.

[0006] There is therefore a need in the art of software verification for a scalable solution to formal verification construction that leverages different formal verification tools to verify UML statecharts from varying design/modeling tools.

Brief Description of the Drawings

[0007] Figure 1 is a flowchart of an example embodiment of a process to formally verify a Unified Modeling Language (UML) statechart.

[0008] Figure 2 is an example embodiment of a computer system that may be used in connection with the formal verification of UML statecharts.

Detailed Description

[0009] In the following detailed description, reference is made to the accompanying drawings that show, by way of illustration, specific embodiments in which the invention may be practiced. These embodiments are described in sufficient detail to enable those skilled in the art to practice the invention. It is to be understood that the various embodiments of the invention, although different, are not necessarily mutually exclusive. For example, a particular feature, structure, or characteristic described herein in connection with one embodiment may be implemented within other embodiments without departing from the scope of the invention. In addition, it is to be understood that the location or arrangement of individual elements within each disclosed embodiment may be modified without departing from the scope of the invention. The following detailed description is, therefore, not to be taken in a limiting sense, and the scope of the present invention is defined only by the appended claims, appropriately interpreted, along with the full range of equivalents to which the claims are entitled. In the drawings, like numerals refer to the same or similar functionality throughout the several views. [0010] An embodiment addresses the shortcomings of the prior art by defining an intermediate language referred to as a Statechart Markup Language (SML). In this embodiment, the SML is an XML-based intermediate language. The means of statechart representation may be generated with UML Statechart modeling tools. In another embodiment, the statechart representation may be generated from a UML exchange standard — XML Metadata Interchange (XMI). Then, by leveraging XSLT (the XML- based functional programming language eXstensible Style Language Transformation), a translator translates the SML into any other text based format (for verification tools). Consequently, an SML document can be translated into the input language of different formal verification tools. In this manner, a statechart diagram may be verified using different formal verification tools (such as SMV or SPIN) through the use of SML. This manner ensures the robustness of the statecharts, and maximizes the verifiability of the statecharts via many different verification tools.

[0011] In contrast to the prior art, embodiments of the invention are not a direct method of formal verification (i.e., building a finite model of a system as a set of states and state transitions and verifying that a desired property holds in a model). Rather, embodiments provide a transformation-based verification framework. This framework formally verifies UML statecharts by leveraging existing UML Statechart design/modeling tools and formal verification tools. Moreover, in contrast to other transformation-based solutions, embodiments of the invention define an XML-based intermediate language for the presentation of statechart modeling. By employing XML/XSLT technology, support for a variety of formal verification tools and a variety of formal UML Statechart presentation formats may be provided. In other prior-art based transformation solutions, transformation is accomplished through the use of traditional programming languages such as C, C++, or Java, and this makes building a new translator for a new input format and output format very difficult. The embodiments of the present invention however, by adopting an XML-based intermediate language and XSLT technology, the solutions are generally more scalable.

[0012] As stated above, the SML language may be implemented in XML. In an embodiment, SML has a root element referred to as a statechart. The statechart root includes a plurality of complex types, and it is through these complex types that a model may be verified. An action type is an executable atomic computation that results in a change in the state of a model or the return of a value. An action may be attached to a transition, and is executed when the transition fires. The action may also appear as entry actions and exit actions of states.

[0013] A Call Event complex type represents the reception of a request to synchronously invoke a specific operation. The expected result is the execution of a sequence of actions that characterize the operation behavior of a particular state. [0014] A Change Event type models an event that occurs when an explicit

Boolean expression becomes true as a result of a change in value of one or more attributes or associations. A Change Event is raised implicitly and is not the result of some explicit Change Event action.

[0015] A Composite State type is a state that contains other state vertices (e.g.

State types and Pseudostate types as explained infra). The association between the composite and the contained vertices is referred to as a composition association. A state vertex can be a part of at most one composite state.

[0016] An Event type specifies a type of observable occurrence. The occurrence that generates an event instance is assumed to take place at an instant in time with no duration. [0017] A Final State type is a special kind of state type and signifies that an enclosing composite state is complete. If the enclosing state is the top state, this signifies that the entire state machine has completed.

[0018] An Operation type signifies an operation in the Call Event type.

[0019] A Parameter type specifies the data that is attached with an Event type.

[0020] A Pseudostate type is an abstraction that encompasses different types of transient vertices in a state machine graph. Psuedostate types are typically used to connect multiple transitions into more complex state transition paths.

[0021] A Signal Event type represents the reception of a particular (asynchronous) signal. The Signal Event is a child of the Event type. Related to the Signal Event type is the Signal type, which is a signal in the Signal Event.

[0022] A Simple State type is a state that does not have substates. It is a child of the State type.

[0023] A State Machine type is a specification that describes all possible behaviors of some dynamic model element. Behaviors are modeled as a traversal of a graph of state nodes interconnected by one or more joined transition arcs that are triggered by the dispatching of series of event instances. During such a transversal, the

State Machine executes a series of actions that are associated with various elements of the

State Machine.

[0024] The State type is an abstract metaclass that models a situation during which some (usually implicit) invariant condition holds. The invariant may represent a static situation such as an object waiting for some external event to occur. In another embodiment, it can model dynamic conditions such as the process of performing some activity. The State is a child of the State Vertex type. The State Vertex type is an abstraction of a node in a state chart graph. The State Vertex can be the source or destination of any number of transitions.

[0025] A Sub State type may appear within a Sub Machine State type, and it represents an actual subvertex contained within the referenced state machine. It may serve as a source or destination of transitions that connect a state vertex in the containing state machine with a subvertex in the referenced State Machine type. [0026] A Sub Machine State type is a syntactical convenience that facilitates reuse and modularity. It is a shorthand that implies a macro-like expansion by another State Machine type and is semantically equivalent to the Composite State type. The State Machine type that is inserted is referred to as the referenced state machine, while the State Machine type that contains the Sub Machine State is referred to as the containing state machine. The same State Machine may be referenced more than once in the context of a single containing state machine. In effect, a Sub Machine State represents a call to a State Machine subroutine with one or more entry and exit points. [0027] A Synch State type is a vertex used for synchronizing the concurrent regions of a state machine. It is different from a state in the sense that it is not mapped to a Boolean value {e.g. active, not active), but rather an integer. A synch state is used in conjunction with forks and joins to insure that one region leaves a particular state or states before another region can enter a particular state or states. The Synch State type is a child of the State Vertex type.

[0028] A Time Event type models the expiration of a specific deadline. The time of occurrence of a time event instance {i.e., the expiration of a deadline) is the same as the time of its reception. However, it is important to note that there may be a variable delay between the time of reception and the time of dispatching {e.g., due to queuing delays).

[0029] A Transition type is a directed relationship between a source state vertex and a target state vertex. It may be part of a compound transition, which takes the State Machine from one state configuration to another, representing the complete response of the state machine to a particular event instance. A Transition Refs type is a reference to a transition. A Transitions type is a Transition's collection.

[0030] Referring now to Figure 1, an embodiment of a formal verification process for a UML statechart is illustrated. Specifically, Figure 1 illustrates a process 100 wherein a UML statechart is created at 110. In an embodiment, the UML statechart may be constructed with a drawing tool such as Microsoft Visio, Rational Rose, or some other graphics tool. The UML statechart is then translated into SML format at 120. In one embodiment, the SML files may be generated manually. In another embodiment, a plug- in may be written to generate an SML file from the visual modeling tool used in step 110. The SML file is then translated into a corresponding target format at 130. This translation is into an existing verification tool's input language format. Examples of popular verification tools are SMV or SPIN. After generation of the target format, existing formal verification tools (i.e., SPIN, SMV) may be used at 140 to verify the model represented by the statechart in 1 10.

[0031] Figure 2 shows a diagrammatic representation of machine in the exemplary form of a computer system 200 within which a set of instructions, for causing the machine to perform any one of the methodologies discussed above, may be executed. In the alternative embodiment, the machine may comprise a network router, a network switch, a network bridge, Personal Digital Assistant (PDA), a cellular telephone, a web appliance or any machine capable of executing a sequence of instructions that specify actions to be taken by the machine.

[0033] The computer system 200 includes a processor 202, a main memory 204 and a static memory 206, which communicate with each other via a bus 208. The computer system 200 may further include a video display unit 210 (e.g., a liquid crystal display (LCD) or a cathode ray tube (CRT)). The computer system 200 also includes an alpha-numeric input device 212 (e.g., a keyboard), a cursor control device 214 (e.g., a mouse), a disk drive unit 216, a signal generation device 220 (e.g., a speaker) and a network interface device 222.

[0034] The disk drive unit 216 includes a computer-readable medium 224 on which is stored a set of instructions (i.e., software) 226 embodying any one, or all, of the methodologies described above. The software 226 is also shown to reside, completely or at least partially, within the main memory 204 and/or within the processor 202. The software 226 may further be transmitted or received via the network interface device 222. For the purposes of this specification, the term " computer-readable medium" shall be taken to include any medium that is capable of storing or encoding a sequence of instructions for execution by the computer and that cause the computer to perform any one of the methodologies of the present invention. The term "computer-readable medium" shall accordingly be taken to included, but not be limited to, solid-state memories, optical and magnetic disks, and carrier wave signals. [0035] Thus, a method to formally verify statecharts has been described. Although the present invention has been described with reference to specific exemplary embodiments, it will be evident that various modifications and changes may be made to these embodiments without departing from the broader spirit and scope of the invention. Accordingly, the specification and drawings are to be regarded in an illustrative rather than a restrictive sense.

Claims

1. A process comprising: creating a statechart; exporting said statechart into an intermediate language; translating said intermediate language into a target format; and verifying said statechart.

2. The process of claim 1, wherein said statechart comprises a UML statechart.

3. The process of claim 1, wherein said intermediate language is XML-based.

4. The process of claim 1, wherein said statechart is created with an electronic drawing tool.

5. The process of claim 1, wherein said target format comprises SMV.

6. The process of claim 1, wherein said target format comprises SPIN.

7. The process of claim 1, wherein said intermediate language comprises a Statechart Markup Language (SML).

8. The process of claim 1, wherein said intermediate language comprises: a root element; one or more complex types; and one or more action types; wherein said verifying occurs via said complex types.

9. The process of claim 8, wherein said intermediate language further comprises: a call event complex type to receive a request to synchronously invoke a specific operation; a change event type to model an event when a Boolean expression becomes true as a result of an attribute or association change; a composite state type comprising state vertices; an event type comprising an observable occurrence; a final state type comprising a signification that a composite state is complete; an operation type coupled with said call event type; a parameter type specifying data in an event type; a pseudostate type comprising types of vertices in a state machine; a signal event type representing the reception of a signal; a simple state type; a state machine type describing behaviors of a model element; a state type comprising a metaclass to model a situation during which an invariant condition exists; a sub state type comprising a subvertex within a state machine; a sub machine state type to facilitate reuse and modularity; a synch state type comprising a vertex for synchronizing regions of a state machine; a time event type to model the expiration of a specific deadline; and a transition type comprising a relationship between a source state vertex and a target state vertex.

10. A machine readable medium comprising instructions thereon for executing a process comprising: creating a statechart; exporting said statechart into an intermediate language; translating said intermediate language into a target format; and verifying said statechart.

11. The machine readable medium of claim 10, wherein said statechart comprises a UML statechart.

12. The machine readable medium of claim 10, wherein said intermediate language is XML-based.

13. The machine readable medium of claim 10, wherein said statechart is created with an electronic drawing tool.

14. The machine readable medium of claim 10, wherein said target format comprises

SMV.

15. The machine readable medium of claim 10, wherein said target format comprises SPIN.

16. The machine readable medium of claim 10, wherein said intermediate language comprises a Statechart Markup Language (SML).

17. The machine readable medium of claim 10, wherein said intermediate language comprises: a root element; one or more complex types; and one or more action types; wherein said verifying occurs via said complex types.

18. The machine readable medium of claim 17, wherein said intermediate language further comprises: a call event complex type to receive a request to synchronously invoke a specific operation; a change event type to model an event when a Boolean expression becomes true as a result of an attribute or association change; a composite state type comprising state vertices; an event type comprising an observable occurrence; a final state type comprising a signification that a composite state is complete; an operation type coupled with said call event type; a parameter type specifying data in an event type; a pseudostate type comprising types of vertices in a state machine; a signal event type representing the reception of a signal; a simple state type; a state machine type describing behaviors of a model element; a state type comprising a metaclass to model a situation during which an invariant condition exists; a sub state type comprising a subvertex within a state machine; a sub machine state type to facilitate reuse and modularity; a synch state type comprising a vertex for synchronizing regions of a state machine; a time event type to model the expiration of a specific deadline; and a transition type comprising a relationship between a source state vertex and a target state vertex.

19. A process comprising: creating a UML statechart in a computer memory; exporting said UML statechart into an XML-based intermediate language; translating said XML-based intermediate language into a target format; and verifying said UML statechart.

20. The process of claim 19, wherein said XML-based intermediate language comprises: a root element; one or more complex types; and one or more action types; wherein said verifying occurs via said complex types.