The controller - provides 5 services in parallel

This system consists of a control component which provides 5 services (service1, ..., service5) in parallel and user components, which require the services sequentially.

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

The control component: The control component (Subject) models five independent parallel methods (services), service1(), ...,service5().

A user component: User can call any of the 5 services, and then it must wait for the return of the service.

Numbers of states: The control component model has 2⁵ = 32 states and the model of user component has 6 states.

CI model of the system with 9 users: Example005.cdve.

Models

Component-Interaction automata model / Labelled Kripke structure model:

TODO TODO

Size

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

n	1	2	3	4	5	6	7	8	9
size of the system with n users	6	31	136	501	1 546	4 051	9 276	19 080	36 046

Extended information

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

Cutoffs

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

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 
(11112)  || * - - - - 1

describes that if the control component is in the state (1, 1, 1, 1, 2) then it is possible that an arbitrary number of users are in the local state 1 (symbol "*"), no user is in the states 2,3,4,3 (symbol "-"), and exactly one user is in the state 6 (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                                                                              
(11111)  ||  * - - - - -            ((11111),2),   ((11111),3),   ((11111),4),   ((11111),5),   ((11111),6),
(11112)  ||  * - - - - 1            ((11112),2),   ((11112),3),   ((11112),4),   ((11112),5),   ((11112),6,6),
(11121)  ||  * - - - 1 -            ((11121),2),   ((11121),3),   ((11121),4),   ((11121),5,5), ((11121),6),
(11122)  ||  * - - - 1 1            ((11122),2),   ((11122),3),   ((11122),4),   ((11122),5,5), ((11122),6,6),
(11211)  ||  * - - 1 - -            ((11211),2),   ((11211),3),   ((11211),4,4), ((11211),5),   ((11211),6),
(11212)  ||  * - - 1 - 1            ((11212),2),   ((11212),3),   ((11212),4,4), ((11212),5),   ((11212),6,6),
(11221)  ||  * - - 1 1 -            ((11221),2),   ((11221),3),   ((11221),4,4), ((11221),5,5), ((11221),6),
(11222)  ||  * - - 1 1 1            ((11222),2),   ((11222),3),   ((11222),4,4), ((11222),5,5), ((11222),6,6),
(12111)  ||  * - 1 - - -            ((12111),2),   ((12111),3,3), ((12111),4),   ((12111),5),   ((12111),6),
(12112)  ||  * - 1 - - 1            ((12112),2),   ((12112),3,3), ((12112),4),   ((12112),5),   ((12112),6,6),
(12121)  ||  * - 1 - 1 -            ((12121),2),   ((12121),3,3), ((12121),4),   ((12121),5,5), ((12121),6),
(12122)  ||  * - 1 - 1 1            ((12122),2),   ((12122),3,3), ((12122),4),   ((12122),5,5), ((12122),6,6),
(12211)  ||  * - 1 1 - -            ((12211),2),   ((12211),3,3), ((12211),4,4), ((12211),5),   ((12211),6),
(12212)  ||  * - 1 1 - 1            ((12212),2),   ((12212),3,3), ((12212),4,4), ((12212),5),   ((12212),6,6),
(12221)  ||  * - 1 1 1 -            ((12221),2),   ((12221),3,3), ((12221),4,4), ((12221),5,5), ((12221),6),
(12222)  ||  * - 1 1 1 1            ((12222),2),   ((12222),3,3), ((12222),4,4), ((12222),5,5), ((12222),6,6),
(21111)  ||  * 1 - - - -            ((21111),2,2), ((21111),3),   ((21111),4),   ((21111),5),   ((21111),6),
(21112)  ||  * 1 - - - 1            ((21112),2,2), ((21112),3),   ((21112),4),   ((21112),5),   ((21112),6,6),
(21121)  ||  * 1 - - 1 -            ((21121),2,2), ((21121),3),   ((21121),4),   ((21121),5,5), ((21121),6),
(21122)  ||  * 1 - - 1 1            ((21122),2,2), ((21122),3),   ((21122),4),   ((21122),5,5), ((21122),6,6),
(21211)  ||  * 1 - 1 - -            ((21211),2,2), ((21211),3),   ((21211),4,4), ((21211),5),   ((21211),6),
(21212)  ||  * 1 - 1 - 1            ((21212),2,2), ((21212),3),   ((21212),4,4), ((21212),5),   ((21212),6,6),
(21221)  ||  * 1 - 1 1 -            ((21221),2,2), ((21221),3),   ((21221),4,4), ((21221),5,5), ((21221),6),
(21222)  ||  * 1 - 1 1 1            ((21222),2,2), ((21222),3),   ((21222),4,4), ((21222),5,5), ((21222),6,6),
(22111)  ||  * 1 1 - - -            ((22111),2,2), ((22111),3,3), ((22111),4),   ((22111),5),   ((22111),6),
(22112)  ||  * 1 1 - - 1            ((22112),2,2), ((22112),3,3), ((22112),4),   ((22112),5),   ((22112),6,6),
(22121)  ||  * 1 1 - 1 -            ((22121),2,2), ((22121),3,3), ((22121),4),   ((22121),5,5), ((22121),6),
(22122)  ||  * 1 1 - 1 1            ((22122),2,2), ((22122),3,3), ((22122),4),   ((22122),5,5), ((22122),6,6),
(22211)  ||  * 1 1 1 - -            ((22211),2,2), ((22211),3,3), ((22211),4,4), ((22211),5),   ((22211),6),
(22212)  ||  * 1 1 1 - 1            ((22212),2,2), ((22212),3,3), ((22212),4,4), ((22212),5),   ((22212),6,6),
(22221)  ||  * 1 1 1 1 -            ((22221),2,2), ((22221),3,3), ((22221),4,4), ((22221),5,5), ((22221),6),
(22222)  ||  * 1 1 1 1 1            ((22222),2,2), ((22222),3,3), ((22222),4,4), ((22222),5,5), ((22222),6,6),

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