Show Me

As a protocol system is created on one or more Edit sheets, the architect needs to have confidence that the design is correct. The best way to do this is observe the protocol in action.

"The designer has a particular behavior in mind; seeing repeated simulations match that behavior is the most convincing demonstration that the architecture is defined as intended."

The above quote is from a paper by A.A.R. Cockburn, et al., researchers for IBM's Zurich Zurich Research Laboratory in the the 1990's. This team's published work provided much inspiration to the development of ProtoCollum.

The protocol is tested by creating scenarios on Test sheets. In a test scenario, actual instances of the architecture objects are placed into a simulation environment. The user directs the flow of the scenario by controlling the order in which messages arrive at the various Processing Entity (PE) objects.

The animated diagram shows the interactive nature of the Test sheet that allows a designer to "play" with the protocol design. The following steps are shown:

1. The user chooses a destination PE in order to complete the connection of a message. The message arrival causes the action code of the related guard Event to execute.
2. The simulation engine checks all of the rules associated with the message Connect (as determined by the architecture), to see if any rule will now trigger. If a rule triggers, the rule name will be shown and the action events will also be posted.
3. The rule ruleAttach has triggered and it has two messages it wants to send. The user has selected one of these messages and is in the process of selecting a destination PE.

Can You Prove That

An alternative to the dynamic testing enabled by ProtoCollum is doing static analysis with formal verification tools. These tools do an exhaustive examination of the given state space and check for assertion violations. While this is a very powerful method, it only works on what is there, it cannot work on what is missing. Formal methods cannot detect whether the design is really accomplishing the task the architect intended (as opposed to busily and "correctly" doing the wrong task).

A small example of this was seen while using ProtoCollum to model a file-transfer-protocol described in a formal verification book. In Chapter 7 the protocol is specified in a formal language called SPIN. Yet after creating a ProtoCollum model for the FTP, the very first test scenario revealed an omission: At the completion of the file transfer the originating file is not closed on the file server.

Due to the graphical nature of the test scenario, not only is it easy to see the missing state change, but it is also easy to see a couple different places where a message could be generated to tell the file server to close the file.

This FTP model and test scenarios are included in the file holz_ch7.mps which comes in the demo/ area of the download package.

A discussion of how ProtoCollum and formal tools might work together is found here.