Token and its support

C-U system Token and its support is a part of a model of the prototype implementation of a payment system for public Internet access on airports [1] modeled using behaviour protocols [2]. It models a system where clients (represented as instances of component Token) of several air-carriers can have access to the Internet. Clients have to authenticate themselves or pay for the service before they are able to establish communication with the Internet. The client's Internet session starts when the client authenticates and terminates after some amount of time or when the client itself terminates the session.

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

The control component (implementation of a payment system) models three independent methods and hence its model consists of three independent parallel parts. First of them is able to receive an information that a Token is invalided (the terminating phase of an Internet session is successfully finished). The second is for changing the prepaid time during the invalidating of the Token (terminating of an Internet session). The last is for creating a Token (it represents starting an Internet session) and for starting of invalidating of the Token (it represents terminating of the session). There are two types of a session - a prepaid session and free session (clients with a valid fly ticket for first class or business class have full Internet access during the ticket validity period free of charge).

A user component (Token) models a client of the system. At first the client must be initialized and then it models an initialized Internet session. They are two possibilities of Internet sessions - a prepaid session or a free session. There are two possibilities how to terminate an existing session - the client(=Token) terminates the session or the system terminates the session (because the prepaid time is used up or fly ticket becomes invalidated). If the client terminates the session, then after some time the control component detects it and sends to the Token an action InvalidateAndSave. After that, if the session is prepaid, the Token changes the prepaid time (actions adjustPrepaidTime, adjustPrepaidTime'). Subsequently the Token announces that it is invalidated (actions tokenInvalidated, tokenInvalidated') and returns InvalidateAndSave'. If the system terminates the session, if the session is prepaid, the client changes the prepaid time (actions adjustPrepaidTime, adjustPrepaidTime'). Subsequently the Token announces that it is invalidated (actions tokenInvalidated, tokenInvalidated').

The model of the control component has 2*2*4 = 16 states and the model of a user has 17 states.

Models

Component-Interaction automata model / Labelled Kripke structure model:

CI control component model - Subject CI user model - Observer

Size

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

n	1	2	3	4	5	6
size of the system with n users	17	207	2 063	18 085	145 125	1 091 875

Extended information

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

Cutoffs

l	0	1	2	3	4	5
Cutoff	3	4	5	6	7	8

Reachable states

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

      0   1   2   3   4   5   6   7   8   9   A   B   C   D   E   F   G                 
002 | * | - | * | - | * | - | - | - | 1 | - | - | - | * | - | - | - | - |

describe that of the control component is in the state (0, 0, 2) then it is possible that arbitrary number of users are in the local states 0, 2, 4, C (symbol "*"), no user is in the states 1, 3, 5, ... (symbol "-"), and exactly one user must be in the state 8 (symbol "1").

      0   1   2   3   4   5   6   7   8   9   A   B   C   D   E   F   G
000 | * | - | * | - | * | - | - | - | - | - | - | - | * | - | - | - | - | 
001 | * | 1 | * | - | * | - | - | - | - | - | - | - | * | - | - | - | - |  
002 | * | - | * | - | * | - | 1 | - | - | - | - | - | * | - | - | - | - | 
002 | * | - | * | - | * | - | - | - | 1 | - | - | - | * | - | - | - | - | 
002 | * | - | * | - | * | - | - | - | - | - | 1 | - | * | - | - | - | - | 
002 | * | - | * | - | * | - | - | - | - | - | - | - | * | - | 1 | - | - | 
002 | * | - | * | - | * | - | - | - | - | - | - | - | * | - | - | - | 1 |  
003 | * | - | * | - | * | - | - | - | - | - | - | 1 | * | - | - | - | - |
010 | * | - | * | 1 | * | - | - | - | - | - | - | - | * | - | - | - | - |
011 | * | 1 | * | 1 | * | - | - | - | - | - | - | - | * | - | - | - | - |
012 | * | - | * | 1 | * | - | 1 | - | - | - | - | - | * | - | - | - | - |
012 | * | - | * | 1 | * | - | - | - | 1 | - | - | - | * | - | - | - | - |
012 | * | - | * | 1 | * | - | - | - | - | - | 1 | - | * | - | - | - | - |
012 | * | - | * | 1 | * | - | - | - | - | - | - | - | * | - | 1 | - | - |
012 | * | - | * | 1 | * | - | - | - | - | - | - | - | * | - | - | - | 1 | 
012 | * | - | * | - | * | - | - | 1 | - | - | - | - | * | - | - | - | - |
013 | * | - | * | 1 | * | - | - | - | - | - | - | 1 | * | - | - | - | - |
100 | * | - | * | - | * | 1 | - | - | - | - | - | - | * | - | - | - | - |
100 | * | - | * | - | * | - | - | - | - | - | - | - | * | 1 | - | - | - |
101 | * | 1 | * | - | * | 1 | - | - | - | - | - | - | * | - | - | - | - |
101 | * | 1 | * | - | * | - | - | - | - | - | - | - | * | 1 | - | - | - |
102 | * | - | * | - | * | 1 | 1 | - | - | - | - | - | * | - | - | - | - |
102 | * | - | * | - | * | 1 | - | - | 1 | - | - | - | * | - | - | - | - |
102 | * | - | * | - | * | 1 | - | - | - | - | 1 | - | * | - | - | - | - |
102 | * | - | * | - | * | 1 | - | - | - | - | - | - | * | - | 1 | - | - |
102 | * | - | * | - | * | 1 | - | - | - | - | - | - | * | - | - | - | 1 |
102 | * | - | * | - | * | - | 1 | - | - | - | - | - | * | 1 | - | - | - |
102 | * | - | * | - | * | - | - | - | 1 | - | - | - | * | 1 | - | - | - |
102 | * | - | * | - | * | - | - | - | - | - | 1 | - | * | 1 | - | - | - |
102 | * | - | * | - | * | - | - | - | - | - | - | - | * | 1 | 1 | - | - |
102 | * | - | * | - | * | - | - | - | - | - | - | - | * | 1 | - | - | 1 |
102 | * | - | * | - | * | - | - | - | - | 1 | - | - | * | - | - | - | - |
102 | * | - | * | - | * | - | - | - | - | - | - | - | * | - | - | 1 | - |
103 | * | - | * | - | * | 1 |   | - |   | - |   | 1 | * | - |   | - |   |
103 | * | - | * | - | * | - |   | - |   | - |   | 1 | * | 1 |   | - |   |
110 | * | - | * | 1 | * | 1 | - | - | - | - | - | - | * | - | - | - | - |
110 | * | - | * | 1 | * | - | - | - | - | - | - | - | * | 1 | - | - | - |
111 | * | 1 | * | 1 | * | 1 | - | - | - | - | - | - | * | - | - | - | - |
111 | * | 1 | * | 1 | * | - | - | - | - | - | - | - | * | 1 | - | - | - |
112 | * | - | * | - | * | 1 | - | 1 | - | - | - | - | * | - | - | - | - |
112 | * | - | * | - | * | - | - | 1 | - | - | - | - | * | 1 | - | - | - |
112 | * | - | * | 1 | * | - | - | - | - | 1 | - | - | * | - | - | - | - |
112 | * | - | * | 1 | * | - | - | - | - | - | - | - | * | - | - | 1 | - |
112 | * | - | * | 1 | * | 1 | 1 | - | - | - | - | - | * | - | - | - | - |
112 | * | - | * | 1 | * | 1 | - | - | 1 | - | - | - | * | - | - | - | - |
112 | * | - | * | 1 | * | 1 | - | - | - | - | 1 | - | * | - | - | - | - |
112 | * | - | * | 1 | * | 1 | - | - | - | - | - | - | * | - | 1 | - | - |
112 | * | - | * | 1 | * | 1 | - | - | - | - | - | - | * | - | - | - | 1 |
112 | * | - | * | 1 | * | - | 1 | - | - | - | - | - | * | 1 | - | - | - |
112 | * | - | * | 1 | * | - | - | - | 1 | - | - | - | * | 1 | - | - | - |
112 | * | - | * | 1 | * | - | - | - | - | - | 1 | - | * | 1 | - | - | - |
112 | * | - | * | 1 | * | - | - | - | - | - | - | - | * | 1 | 1 | - | - |
112 | * | - | * | 1 | * | - | - | - | - | - | - | - | * | 1 | - | - | 1 |
113 | * | - | * | 1 | * | 1 | - | - | - | - | - | 1 | * | - | - | - | - |
113 | * | - | * | 1 | * | - | - | - | - | - | - | 1 | * | 1 | - | - | - |

"*" - an arbitrary number of users, 
"-" - no user,
"1" - exactly one user.

Unreachable l+1-tuples

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

      0   1   2   3   4   5   6   7   8   9   A   B   C   D   E   F   G
000 | * | - | * | - | * | - | - | - | - | - | - | - | * | - | - | - | - | 
unreachable tuples: (000,1), (000,3), (000,5), (000,6), (000,7), (000,8), (000,9), (000,A), (000,B), (000,D), (000,E), (000,F), (000,G)

      0   1   2   3   4   5   6   7   8   9   A   B   C   D   E   F   G 
001 | * | 1 | * | - | * | - | - | - | - | - | - | - | * | - | - | - | - |  
unreachable tuples: (001,3), (001,5), (001,6), (001,7), (001,8), (001,9), (001,A), (001,B), (001,D), (001,E), (001,F), (001,G), 
                    (001,1,1)

      0   1   2   3   4   5   6   7   8   9   A   B   C   D   E   F   G 
002 | * | - | * | - | * | - | 1 | - | - | - | - | - | * | - | - | - | - | 
002 | * | - | * | - | * | - | - | - | 1 | - | - | - | * | - | - | - | - | 
002 | * | - | * | - | * | - | - | - | - | - | 1 | - | * | - | - | - | - | 
002 | * | - | * | - | * | - | - | - | - | - | - | - | * | - | 1 | - | - | 
002 | * | - | * | - | * | - | - | - | - | - | - | - | * | - | - | - | 1 |  
unreachable tuples: (002,1), (002,3), (002,5), (002,7), (002,9), (002,B), (002,D), (002,F)
                    (002,6,6), (002,8,8), (002,A,A),(002,E,E),(002,G,G),
                    (002,6,8),(002,6,A),(002,6,E),(002,6,G), (002,8,A),(002,8,E),(002,8,G),(002,A,E),(002,A,G),(002,E,G)

      0   1   2   3   4   5   6   7   8   9   A   B   C   D   E   F   G 
003 | * | - | * | - | * | - | - | - | - | - | - | 1 | * | - | - | - | - |
unreachable tuples: (003,1), (003,3), (003,5), (003,6), (003,7), (003,8), (003,9), (003,A), (003,D), (003,E), (003,F), (003,G), 
                    (003,B,B) 

      0   1   2   3   4   5   6   7   8   9   A   B   C   D   E   F   G 
010 | * | - | * | 1 | * | - | - | - | - | - | - | - | * | - | - | - | - |
unreachable tuples: (010,1), (010,5), (010,6), (010,7), (010,8), (010,9), (010,A), (010,B), (010,D), (010,E), (010,F), (010,G), 
                    (010,3,3)

      0   1   2   3   4   5   6   7   8   9   A   B   C   D   E   F   G 
011 | * | 1 | * | 1 | * | - | - | - | - | - | - | - | * | - | - | - | - |
unreachable tuples: (011,5), (011,6), (011,7), (011,8), (011,9), (011,A), (011,B), (011,D), (011,E), (011,F), (011,G),
                    (011,1,1), (011,3,3)

      0   1   2   3   4   5   6   7   8   9   A   B   C   D   E   F   G 
012 | * | - | * | 1 | * | - | 1 | - | - | - | - | - | * | - | - | - | - |
012 | * | - | * | 1 | * | - | - | - | 1 | - | - | - | * | - | - | - | - |
012 | * | - | * | 1 | * | - | - | - | - | - | 1 | - | * | - | - | - | - |
012 | * | - | * | 1 | * | - | - | - | - | - | - | - | * | - | 1 | - | - |
012 | * | - | * | 1 | * | - | - | - | - | - | - | - | * | - | - | - | 1 | 
012 | * | - | * | - | * | - | - | 1 | - | - | - | - | * | - | - | - | - |
unreachable tuples: (012,1), (012,5), (012,9), (012,B), (012,D), (012,F), 
                    (012,3,3), (012,6,6),(012,7,7),(012,8,8), (012,A,A),(012,E,E),(012,G,G),
                    (012,7,3), (012,7,6),(012,7,8),(012,7,A),(012,7,E),(012,7,G),
                    (012,6,8), (012,6,A), (012,6,E), (012,6,G), (012,8,A),(012,8,E), (012,8,G), (012,A,E), (012,A,G), (012,E,G)

      0   1   2   3   4   5   6   7   8   9   A   B   C   D   E   F   G 
013 | * | - | * | 1 | * | - | - | - | - | - | - | 1 | * | - | - | - | - |
unreachable tuples: (000,1), (000,5), (000,6), (000,7), (000,8), (000,9), (000,A), (000,D), (000,E), (000,F), (000,G),
                    (000,3,3), (000,B,B) 

      0   1   2   3   4   5   6   7   8   9   A   B   C   D   E   F   G 
100 | * | - | * | - | * | 1 | - | - | - | - | - | - | * | - | - | - | - |
100 | * | - | * | - | * | - | - | - | - | - | - | - | * | 1 | - | - | - |
unreachable tuples: (100,1), (100,3), (100,6), (100,7), (100,8), (100,9), (100,A), (100,B), (100,E), (100,F), (100,G)
                    (100,5,5), (100,D,D)
                    (100,5,D)

      0   1   2   3   4   5   6   7   8   9   A   B   C   D   E   F   G 
101 | * | 1 | * | - | * | 1 | - | - | - | - | - | - | * | - | - | - | - |
101 | * | 1 | * | - | * | - | - | - | - | - | - | - | * | 1 | - | - | - |
unreachable tuples: (101,3), (101,6), (101,7), (101,8), (101,9), (101,A), (101,B), (101,E), (101,F), (101,G)
                    (101,1,1), (101,5,5), (101,D,D)
                    (101,5,D)

      0   1   2   3   4   5   6   7   8   9   A   B   C   D   E   F   G 
102 | * | - | * | - | * | 1 | 1 | - | - | - | - | - | * | - | - | - | - |
102 | * | - | * | - | * | 1 | - | - | 1 | - | - | - | * | - | - | - | - |
102 | * | - | * | - | * | 1 | - | - | - | - | 1 | - | * | - | - | - | - |
102 | * | - | * | - | * | 1 | - | - | - | - | - | - | * | - | 1 | - | - |
102 | * | - | * | - | * | 1 | - | - | - | - | - | - | * | - | - | - | 1 |
102 | * | - | * | - | * | - | 1 | - | - | - | - | - | * | 1 | - | - | - |
102 | * | - | * | - | * | - | - | - | 1 | - | - | - | * | 1 | - | - | - |
102 | * | - | * | - | * | - | - | - | - | - | 1 | - | * | 1 | - | - | - |
102 | * | - | * | - | * | - | - | - | - | - | - | - | * | 1 | 1 | - | - |
102 | * | - | * | - | * | - | - | - | - | - | - | - | * | 1 | - | - | 1 |
102 | * | - | * | - | * | - | - | - | - | 1 | - | - | * | - | - | - | - |
102 | * | - | * | - | * | - | - | - | - | - | - | - | * | - | - | 1 | - |
unreachable tuples:  (102,1), (102,3), (102,7), (102,B)
                     (102,5,5), (102,6,6), (102,8,8), (102,9,9), (102,A,A), (102,D,D), (102,E,E), (102,F,F), (102,G,G),
                     (102,9,5), (102,9,6), (102,9,8), (102,9,A), (102,9,D), (102,9,E), (102,9,F), (102,9,G),
                     (102,F,5), (102,F,6), (102,F,8), (102,F,A), (102,F,D), (102,F,E), (102,F,G),
                     (102,6,8), (102,6,A), (102,6,E), (102,6,G), (102,8,A), (102,8,E), (102,8,G), (102,A,E), (102,A,G), (102,E,G),
                     (102,5,D)
                     
      0   1   2   3   4   5   6   7   8   9   A   B   C   D   E   F   G 
103 | * | - | * | - | * | 1 | - | - | - | - | - | 1 | * | - | - | - | - |
103 | * | - | * | - | * | - | - | - | - | - | - | 1 | * | 1 | - | - | - |
unreachable tuples:  (103,1), (103,3), (103,6), (103,7), (103,8), (103,9), (103,A), (103,E), (103,F), (103,G)
                     (103,5,5), (103,D,D), (103,B,B)
                     (103,5,D)

      0   1   2   3   4   5   6   7   8   9   A   B   C   D   E   F   G 
110 | * | - | * | 1 | * | 1 | - | - | - | - | - | - | * | - | - | - | - |
110 | * | - | * | 1 | * | - | - | - | - | - | - | - | * | 1 | - | - | - |
unreachable tuples: (110,1), (110,6), (110,7), (110,8), (110,9), (110,A), (110,B), (110,E), (110,F), (110,G)
                    (110,3,3), (110,5,5), (110,D,D),
                    (110,5,D)
 
      0   1   2   3   4   5   6   7   8   9   A   B   C   D   E   F   G 
111 | * | 1 | * | 1 | * | 1 | - | - | - | - | - | - | * | - | - | - | - |
111 | * | 1 | * | 1 | * | - | - | - | - | - | - | - | * | 1 | - | - | - |
unreachable tuples: (111,6), (111,7), (111,8), (111,9), (111,A), (111,B), (111,E), (111,F), (111,G)
                    (111,1,1), (111,3,3), (111,5,5), (111,D,D),
                    (111,5,D)

      0   1   2   3   4   5   6   7   8   9   A   B   C   D   E   F   G 
112 | * | - | * | - | * | 1 | - | 1 | - | - | - | - | * | - | - | - | - |
112 | * | - | * | - | * | - | - | 1 | - | - | - | - | * | 1 | - | - | - |
112 | * | - | * | 1 | * | - | - | - | - | 1 | - | - | * | - | - | - | - |
112 | * | - | * | 1 | * | - | - | - | - | - | - | - | * | - | - | 1 | - |
112 | * | - | * | 1 | * | 1 | 1 | - | - | - | - | - | * | - | - | - | - |
112 | * | - | * | 1 | * | 1 | - | - | 1 | - | - | - | * | - | - | - | - |
112 | * | - | * | 1 | * | 1 | - | - | - | - | 1 | - | * | - | - | - | - |
112 | * | - | * | 1 | * | 1 | - | - | - | - | - | - | * | - | 1 | - | - |
112 | * | - | * | 1 | * | 1 | - | - | - | - | - | - | * | - | - | - | 1 |
112 | * | - | * | 1 | * | - | 1 | - | - | - | - | - | * | 1 | - | - | - |
112 | * | - | * | 1 | * | - | - | - | 1 | - | - | - | * | 1 | - | - | - |
112 | * | - | * | 1 | * | - | - | - | - | - | 1 | - | * | 1 | - | - | - |
112 | * | - | * | 1 | * | - | - | - | - | - | - | - | * | 1 | 1 | - | - |
112 | * | - | * | 1 | * | - | - | - | - | - | - | - | * | 1 | - | - | 1 |
unreachable tuples:  (112,1), (112,B), 
                     (112,3,3),(112,5,5),(112,6,6),(112,7,7),(112,8,8),(112,9,9),(112,A,A),(112,D,D),(112,E,E),(112,F,F),(112,G,G),
                     (112,7,3),(112,7,6),(112,7,8),(112,7,9),(112,7,A),(112,7,E),(112,7,F),(112,7,G)
                     (112,5,D),
                     (112,6,8), (112,6,A), (112,6,E), (112,6,G), (112,8,A), (112,8,E), (112,8,G), (112,A,E), (112,A,G), (112,E,G),
                     (112,9,5),(112,9,6),(112,9,8), (112,9,A),(112,9,D),(112,9,E),(112,9,F),(112,9,G),                
                     (112,F,5),(112,F,6),(112,F,8),(112,F,9),(112,F,A),(112,F,D),(112,F,E),(112,F,G),    

      0   1   2   3   4   5   6   7   8   9   A   B   C   D   E   F   G 
113 | * | - | * | 1 | * | 1 | - | - | - | - | - | 1 | * | - | - | - | - |
113 | * | - | * | 1 | * | - | - | - | - | - | - | 1 | * | 1 | - | - | - |
unreachable tuples: (113,1), (113,6), (113,7), (113,8), (113,9), (113,A), (113,E), (113,F), (113,G)
                    (113,3,3), (113,5,5), (113,B,B), (113,D,D),
                    (113,5,D)

[1] Component reliability extensions for fractal component model. http://kraken.cs.cas.cz/ft/public/public_index.phtml

[2] F. Plasil and S. Visnovsky. Behavior protocols for software components. IEEE Transactions on SW Engineering, 28(11):1056–1076, November 2002.