Protocol Model
A service's protocol defines an order of the operations defined in the service's interface.
For a provided interface, a protocol defines in which order the operations have to be (are assumed to be) invoked in order to provide a correct behavior.
For a required interface, a protocol defines in which order operations will be invoked.
Protocols will be used later for protocol matching and analysis of functional correctness.
In order specify protocols, we will use the Protocol Model, which is created as in the following steps.
- In the Package Explorer, select the project which is created as in Section Creating a New Project.
Then right-click on the model folder and select
New > Other... from the context menu.
- Select Service Specification Environment > Protocol Model > Next
- Define the name of your protocol model by filling the field File name. In our example, the protocol model is called
myProtocol.sse_proto. Important, always the filename extension of your
protocol model should be *.sse_proto.
- The tree editor will look like the picture below.
- To add states and transitions in the tree editor you need to right-click on
the root FSM Protocol, then click New Child
. Then you can choose whether you want to add a new state or a new transition to your model.
- Another representation of the protocol model is the diagram editor. It is easier and faster with the same
functionalities as the tree editor. In order to work with that, you have to right-click on your protocol model
(in our case it is called myProtocol.sse_proto) and then click Initialize sse_proto_diagram diagram file.
-
By using the field File name you can rename your protocol diagram which is based on the protocols model content.
By default, the name of your protocol diagram is the same as the name of the protocol model but it can be changed.
Then click Finish.
-
The editor will look like the picture below. In the right side, you can see the Palette, from where you can select the State or the Transition. With the Protocols Editor, the user can define the order of the Operations which are previously created in Section Creating Signatures .
-
Now you can start to work with the protocol diagram editor. For this, you can select the
State/Transition and then click on the canvas so that a
State/Transition is created.
-
In the Properties View, you can change different properties of a State such as its name. You can also define if the state is an initial or a final state.
-
To the transitions, you have to assign the operations defined in your previously created repository. In order to do so, first you should right-click on the canvas, and select Load Resource from the context menu.
-
In the opened dialogue, you can browse your workspace (/ file system) in order to locate your repository model file and press OK.
-
Now that the repository file is loaded, you can assign an Operation to a transition in the Properties View. In this way, by assigning each operation to a transition, you can define the order of the whole operations. The states represent the state of the system after each operation is executed.
-
In this way, by assigning each operation to a transition, you can define the order of the whole operations. The states represent the state of the system after each operation is executed.