• Ticc
• Examples
• House

We illustrate the modeling language of ticc by means of a simple example: a model of the interaction among contractors fixing a house. The example illustates how Ticc can verify the compatibility of the interaction protocol among entities. The example is available from the Ticc wiki mentioned above. The example models a house with four rooms: K(itchen), L(iving room), B(athroom), (bed)R(oom). Each room may have undergoing repair work; this is tracked by the following global variables:

var K_busy, L_busy, B_busy, R_busy: bool

In each room, four items might need repair: plumb(ing), electr(ical), floor, and wall; their need for repair is tracked by the following global variables:

var K_plumb, K_electr, K_floor, K_wall: bool

Similar variables track the state of L(iving room), B(athroom), and (bed)R(oom). The activity state of the four contractors is tracked by the following global variables:

var plumb_active, electr_active, floor_active, wall_active: bool

A module Breaks models plumbing and electrical failures. A typical action of Breaks is as follows:

  output break_K_plumb : { ~K_plumb ==> K_plumb' & K_floor' & K_wall' }

This action models the fact that, when the plumbing in the kitchen is not broken (~ means "not", and K_plumb tracks whether the K(itchen) plumbing works), then it can break, generating the output action break_K_plumb, and signaling that the kitchen plumbing, floor, and walls need repair. A module Caller calls the repairmen when needed; the plumber is called using the following statement:

  output call_plumb : { ~plumb_active &
         (K_plumb | L_plumb | B_plumb | R_plumb) ==> plumb_active' }

The plumber (and similarly, the other contractors) keep track of whether they are working (via a boolean variable working), as well as the room on which they are working via the local boolean variables Kw, Lw, Bw, Rw. When called, the plumber is initially not working on any room.

  input call_plumb : {local: ~plumb_active ==> working' := false }

When an active plumber, not working on any room, sees that the K(itchen) is unoccupied (~K_busy) and needs repair (K\_plumb), the plumber starts work on the K(itchen):

  output K_start_plumb : 
   { plumb_active & ~working & K_plumb & ~K_busy ==> working' & Kw' & K_busy' }

(similarly for other rooms). While working on the kitchen, the plumber does not expect anybody else to work in it (this is expressed by the guard ~Kw):

  input  K_* : { local: ~Kw ==>  }      //     (*)

The input action K_* is a pattern capable of matching all actions that start with "K_". These actions indicate that someone is starting to work on the kitchen. Hence, this input action requires that, whenever anyone (else) is starting to work on the kitchen, the plumber is not working in the kitchen.

We considered two different electrician modules. A correct implementation, Electrician, checks that the kitchen is free before starting work on the kitchen:

  output K_start_electr :
   { electr_active & ~working & K_electr & ~K_busy ==> working' & Kw' & K_busy' }

Note that above, the variable Kw is local to the electrician, and indicates whether the electrician is working on the kitchen; the equally-named variable Kw in (*) is instead local to the plumber. An incorrect implementation of the electrician, WElectrician, in the rush of getting things done, forgets to check whether somebody else is already at work in the kitchen:

  output K_start_electr :
   { electr_active & ~working & K_electr           ==> working' & Kw' & K_busy' }

TICC is able to detect that the composition of Breaks, Caller,  Plumber, and  Electrician is compatible, whereas it detects that the composition of Breaks, Caller, Plumber, and WElectrician is not. Thus, the protocol violation can be discovered before the complete system, consisting also of modules to repair floors and walls, is constructed. In fact, a simple check would have revealed the incompatibility already in the composition of Plumber and Welectrician. When composing Plumber and Welectrician, Ticc automatically synthesizes the assumption that (i) they are not both called to work, or (ii) no room needs to be repaired by both of them. We also note that the protocol violation is revealed thanks to the input assumption of the correct module Plumber. In the game-based approach that underlies Ticc, the input assumptions of correct modules constrain the protocol of modules that will be later composed into the system, preventing the composition of "rogue" modules. The verification of the correctness of interaction is simply a by-product of composition. This situation should be contrasted to the usual, non-game-based approach to modeling and verification. In the usual approach, detecting incompatibilities requires writing separate specifications of correctness, and can usually be performed only once all components are composed.