Subject-Observer system for m subjects

A description of the Subject - Observer system was published in [1] and its CI model for m subjects was introduced in [2]. It is a system consisting of two types of components - a Subject which encapsulates m states from Observers that access that states.

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

The control component (m subjects) S is a parallel composition of m subjects S¹, S², ..., S^m. Models of subjects Sⁱ are very similar as the model of Subject in Subject-Observer system for 1 subject. As in the C-U Model Subject-Observer system for 1 subject each part of Sⁱ models four independent methods, update(), register(), deregister(), getValue(), ... A difference is that in this case names of actions and the name of the modeled component in Sⁱ are parametrized by i.

Sⁱ

5*2*2*2=40

40^m

An user component (Observer) is a parallel composition of m independent sub-observers. An i-th sub-observer can observe a state maintained by Sⁱ. At first each sub-observer must register to reach the state 3. In this state it is able to accept notification and after that it asks for the value managed by the Subject, or it is able to deregister.

O^j

7^m

Note that the model of this system is very close to m parallel models of the C-U model Subject-Observer system for 1 subject.

Models

Component-Interaction automata model:

CI control component model - Subject CI user model - Observer

Size of state spaces

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

n	1	2	3	4	5	6	7	8
size of the system with n users	35^m	230^m	1 430^m	8 480^m	48 230^m	266 240^m	1 425 920^m	7 454 720^m

Extended information

Cutoffs

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

[1] A. Poetzsch-Heffter, J. Aldrich, M. Barnett, D. Giannakopoulou, G. T. Leavens, and N. Sharygina http://www.cs.ucf.edu/~leavens/SAVCBS/2007/challenge.shtml

[2] P. Varekova and B. Zimmerova. Challenge problem: Subject-observer specification with component-interaction automata. In Proceedings of the ESEC/FSE Workshop on Specification and Verification of Component-Based Systems (SAVCBS'07), pages 75-81, Dubrovnik, Croatia, September 2007.