Coordinator (Sale/CoordinatorEventHandler) system

• Sale/CoordinatorEventHandler models the Trading System published in [2], the Sale/CoordinatorEventHandler model was introduced in [1].

• Modelling: In the model, each method, e.g. publish(), is assigned a tuple of action names: " publish " denotes the call of the method, and " publish' " the return from the method. These two determine the start and the end of the method's execution.

• The control component: The control component in our system is the Coordinator, which is in the Trading System used for managing express checkouts. For this purpose, it keeps a list of sales that were done during last 60 minutes, which helps it to decide whether an express cash desk is needed. The Coordinator model in a cycle waits for receiving the action " event " after that it creates a component sale (actions " sale " and " sale' ") and tests whether an express cash desk is needed. If it is needed the Coordinator publishes it (actions " publish " and " publish' ") and finally is sends the action " event' ". If the express cash desk is not needed the Coordinator only sends the action " event' ". The test whether an express mode is needed means that the Coordinator choose a Sale component, then it tests whether the sale represented by the component expired (" gTS ", " gTS' ") if it is so, it destroys a sale ( " saleD " and " saleD' ") -- not necessary the same component sale. Else if it does not expired the Coordinator asks a component sale for getPaymentMode and getNumberofItems. Then it decides whether an express cash desk is needed or it makes another test.

• A user component: At first a user component (Sale) must be created (actions " sale " and " sale' "). After that it in parallel offers three types of data -- its number of items, payment mode and time of sale until it is destroyed ( " saleD " and " saleD' ").

• Shortcuts: In the models, name of the method getNumberofItems() is shortened to gNI, getPaymentMode() to gPM, getTimeofSale() to gTS, updateStatistics() to uS, and isExpressModeNeeded() to iEMN.

• CoordinatorEventHandler with n Sales:
  

• Numbers of states: The control component (Coordinator) model has 16 states, and user component (Sale) model has 11 states.

• The CI model of the system with 8 users: CoordSale8.cdve.

Models

Component-Interaction automata model / Labelled Kripke structure model:

Size

size of the system with the control component and n users without symmetry reduction.

Extended information

- information involving verification of the reachability properties on the model.

Cutoffs

Reachable states, Unreachable l+1-tuples

- The following table describes all reachable states in the system with any number of clients. For example

      1 2 3 4 5 6 7 8 9 10 11
9  || * - 1 * - - - - - -  - 

describes that if the control component is in the state 9 then it is possible that an arbitrary number of users are in the local states 1, 4 (symbol "*"), no user is in the states 2, 5, 6, 7, 8, 9, 10, 11 (symbol "-"), and exactly one user is in the state 3 (symbol "1").

- The (l+1)-tuples after each line denotes all unreachable (l+1)-tuples which do not contain an unreachable i+1-tuple for some i < l. An interesting fact is that such tuples are only 1+1-tuples and 2+1-tuples

       Reachable states                             Unreachable l+1-tuples 
      1 2 3 4 5 6 7 8 9 10 11
0  || * - - * - - - - -  -  -            (0,2),  (0,3),  (0,5),  (0,6),  (0,7),  (0,8), (0,9), (0,10), (0,11)
1  || * - - * - - - - -  -  -            (1,2),  (1,3),  (1,5),  (1,6),  (1,7),  (1,8), (1,9), (1,10), (1,11)
2  || * - - * - - - - -  -  -            (2,2),  (2,3),  (2,5),  (2,6),  (2,7),  (2,8), (2,9), (2,10), (2,11)
3  || * 1 - * - - - - -  -  -            (3,2,2),(3,3),  (3,5),  (3,6),  (3,7),  (3,8), (3,9), (3,10), (3,11)
4  || * - - + - - - - -  -  -            (4,2),  (4,3),  (4,5),  (4,6),  (4,7),  (4,8), (4,9), (4,10), (4,11)
5  || * - - + - - - - -  -  -            (5,2),  (5,3),  (5,5),  (5,6),  (5,7),  (5,8), (5,9), (5,10), (5,11)
6  || * - - * - - - - -  -  -            (6,2),  (6,3),  (6,5),  (6,6),  (6,7),  (6,8), (6,9), (6,10), (6,11)
7  || * - - * - - 1 - -  -  -            (7,2),  (7,3),  (7,5),  (7,6),  (7,7,7),(7,8), (7,9), (7,10), (7,11)
8  || * - - * - - - - -  -  -            (8,2),  (8,3),  (8,5),  (8,6),  (8,7),  (8,8), (8,9), (8,10), (8,11)
9  || * - 1 * - - - - -  -  -            (9,2),  (9,3,3),(9,5),  (9,6),  (9,7),  (9,8), (9,9), (9,10), (9,11)
A  || * - - * - 1 - - -  -  -            (A,2),  (A,3),  (A,5),  (A,6,6),(A,7),  (A,8), (A,9), (A,10), (A,11)
B  || * - - * 1 - - - -  -  -            (B,2),  (B,3),  (B,5,5),(B,6),  (B,7),  (B,8), (B,9), (B,10), (B,11)
C  || * - - * - - - - -  -  -            (C,2),  (C,3),  (C,5),  (C,6),  (C,7),  (C,8), (C,9), (C,10), (C,11)                     
D  || * - - * - - - - -  -  -            (D,2),  (D,3),  (D,5),  (D,6),  (D,7),  (D,8), (D,9), (D,10), (D,11)
E  || * - - * - - - - -  -  -            (E,2),  (E,3),  (E,5),  (E,6),  (E,7),  (E,8), (E,9), (E,10), (E,11)
F  || * - - * - - - - -  -  -            (F,2),  (F,3),  (F,5),  (F,6),  (F,7),  (F,8), (F,9), (F,10), (F,11)

"*" - an arbitrary number of users, 
"+" - an arbitrary number of users greater than 0, 
"-" - no user,
"1" - exactly one user.

[1] B. Zimmerova and P. Varekova: Reflecting creation and destruction of instances in CBSs modelling and verification. In Proceedings of the Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 07), pages 257 - 264, Znojmo, Czech Republic, 2007.

[2] B. Zimmerova, P. Varekova, N. Benes, I. Cerna, L. Brim, and J. Sochor. The Common Component Modeling Example: Comparing Software Component Models, chapter Component-Interaction Automata Approach (CoIn). To appear in LNCS, 2007.