TorX examples

During the Côte de Resyste project a number of academic case studies have been performed. Some of them we used for teaching purposes, i.e. in the course testing techniques, and others are developed to test/check/improve the TorX tool set. These examples can be downloaded now, see the TorX download page.

Here is a list of TorX examples available:

• CHOCLIQ
• COFFEE
• CONFPROT
• REFUND
• UPORDOWN

Coffee machines

The CHOCLIQ and COFFEE examples are used for the course testing techniques. The purpose of these examples was to show the underlying testing theory in a small sized practical example with TorX.

Chat-Box protocol

The conference protocol was throughout the whole Côte de Resyste project the implementation to test idea's upon. This lead to the case study example: CONFPROT. The CONFPROT example contains two implementations of the protocol. The first is an implementation of the plain protocol itself as it was given in the course protocol implementation. This version is used with the TorX configuration files in the CONFPROT directory that do not contain the string ``.cov''. The second implementation of the conference protocol emits coverage information that can be used for coverage measurement during a test session. This version is used with the TorX configuration files in the CONFPROT directory that do contain the string ``.cov''. Finally, in addition to the CADP-based primer for LOTOS, there is also one based on SMILE, in CONFPROT/SPEC/LOTOS-SMILE. Note, at the time of writing, the SMILE version that is needed for this has not yet been released. Whereas the CADP primer generates (relatively) huge lists of actions (stimuli and observations) if there are un-instantiated (free) variables in the actions in the specification (becauses CADP simply enumerates all possible actions with all possible values), the SMILE primer works in a more symbolic way, by keeping the variables in the actions, and only (laziliy) instantiating them just before the action is ``done''. In addition, the SMILE primer is more efficient with memory but slower.

Up or Down?

The UPORDOWN example was developed to show how the STDIN and STDOUT of the implementation can be connected to the testing tool TorX.

Coffee, or Refund?

The REFUND example shows a few small .lts specifications of a coffee machine that, after a coin is inserted, either, if a button is pressed in time, serves coffee, or, if not, times out and returns (refunds) the coin.

Prev	Table of Contents	Next
Chapter 6: Using TorX		Chapter 8: TorX Tutorial