Simple Subject-Observer system for 1 subject

• The Subject - Observer system is a simple version of the system published in [1] with 1 subject. Its CI model is based on the model introduced in [2]. It is a system consisting of two types of components - a Subject which encapsulates some state from Observers that access that state.

• 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 (Subject) models three independent methods, update(), registering(), getValue(), and hence its model consists of three independent parallel parts. In the figure bellow, they are denoted as S₁, S₂, S₃.

On the update() method (automaton S₁), the Subject first receives the method call, confirms its return (to allow the updater to continue its execution while the notifications are delivered, which is common in Subject-Observer communicational models) and then takes care about notifying the Observers. This proceeds in two loops separated by internal actions. The first loop distributes the notification to the Observers, the second confirms termination of notifications. This allows the Observers to execute bodies of their methods in parallel. More, the confirmation ((-,notify',α) in CI model and (notify',?) in LKS model) is allowed also in other states than 5. This protects the system from deadlock of the Observers that do not manage to synchronize with the Subject before it leaves the state 5. Note that the composition with Observers using a handshake-like composition (required synchronization of complementary labels, which are removed and only synchronized internal labels remain) includes paths representing that 0, 1, 2, ..., all registered Observers are notified. However no Observer can be notified twice. This confirms to the at most once constraint, which will be verified later in this text.

On the remaining registering() method (automaton S₂) the Subject enable to register or deregister. In one time there is possible to register a user or to deregister a user. For both services the Subject only receives the call and then returns that it was successfully done.

On the getValue() method (automaton S₃) the Subject only receives the call and then returns. More interesting behaviour could be inserted on the place of state 2.

The model of part S₁ has 5 sates, the model of part S₂ has 3 sates and the model of part S₃ has 2 sates, thus the whole control component model has 5*3*2 = 30 states.

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
(3, 3, 1)  || * - * 1 * - *              ((3,3,1),2),   ((3,3,1),4,4), ((3,3,1),6)          

describe that of the control component is in the state (3, 3, 1) then it is possible that arbitrary number of users are in the local states 1, 3, 5, 7 (symbol "*"), no user is in the states 2, 6 (symbol "-"), and exactly one user must be in the state 4 (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. 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                                                                              
(1, 1, 1)  || * - * - * - *              ((1,1,1),2),   ((1,1,1),4),   ((1,1,1),6)         
(1, 2, 1)  || * 1 * - * - *              ((1,2,1),2,2), ((1,2,1),4),   ((1,2,1),6)        
(1, 3, 1)  || * - * 1 * - *              ((1,3,1),2),   ((1,3,1),4,4), ((1,3,1),6)          
(1, 1, 2)  || * - * - * 1 *              ((1,1,2),2),   ((1,1,2),4),   ((1,1,2),6,6)         
(1, 2, 2)  || * 1 * - * 1 *              ((1,2,2),2,2), ((1,2,2),4),   ((1,2,2),6,6)          
(1, 3, 2)  || * - * 1 * 1 *              ((1,3,2),2),   ((1,3,2),4,4), ((1,3,2),6,6)          
(2, 1, 1)  || * - * - * - *              ((2,1,1),2),   ((2,1,1),4),   ((2,1,1),6)         
(2, 2, 1)  || * 1 * - * - *              ((2,2,1),2,2), ((2,2,1),4),   ((2,2,1),6)        
(2, 3, 1)  || * - * 1 * - *              ((2,3,1),2),   ((2,3,1),4,4), ((2,3,1),6)          
(2, 1, 2)  || * - * - * 1 *              ((2,1,2),2),   ((2,1,2),4),   ((2,1,2),6,6)         
(2, 2, 2)  || * 1 * - * 1 *              ((2,2,2),2,2), ((2,2,2),4),   ((2,2,2),6,6)          
(2, 3, 2)  || * - * 1 * 1 *              ((2,3,2),2),   ((2,3,2),4,4), ((2,3,2),6,6)          
(3, 1, 1)  || * - * - * - *              ((3,1,1),2),   ((3,1,1,1),4), ((3,1,1),6)         
(3, 2, 1)  || * 1 * - * - *              ((3,2,1),2,2), ((3,2,1),4),   ((3,2,1),6)        
(3, 3, 1)  || * - * 1 * - *              ((3,3,1),2),   ((3,3,1),4,4), ((3,3,1),6)          
(3, 1, 2)  || * - * - * 1 *              ((3,1,2),2),   ((3,1,2),4),   ((3,1,2),6,6)         
(3, 2, 2)  || * 1 * - * 1 *              ((3,2,2),2,2), ((3,2,2),4),   ((3,2,2),6,6)          
(3, 3, 2)  || * - * 1 * 1 *              ((3,3,2),2),   ((3,2,3),4,4), ((3,2,3),6,6)          
(4, 1, 1)  || * - * - * - *              ((4,1,1),2),   ((4,1,1),4),   ((4,1,1),6)         
(4, 2, 1)  || * 1 * - * - *              ((4,2,1),2,2), ((4,2,1),4),   ((4,2,1),6)        
(4, 3, 1)  || * - * 1 * - *              ((4,3,1),2),   ((4,3,2),4,4), ((4,3,1),6)          
(4, 1, 2)  || * - * - * 1 *              ((4,1,2),2),   ((4,1,2),4),   ((4,1,2),6,6)         
(4, 2, 2)  || * 1 * - * 1 *              ((4,2,2),2,2), ((4,2,2),4),   ((4,2,2),6,6)          
(4, 3, 2)  || * - * 1 * 1 *              ((4,3,2),2),   ((4,3,2),4,4), ((4,3,2),6,6)          
(5, 1, 1)  || * - * - * - *              ((5,1,1),2),   ((5,1,1),4),   ((5,1,1),6)         
(5, 2, 1)  || * 1 * - * - *              ((5,2,1),2,2), ((5,2,1),4),   ((5,2,1),6)        
(5, 3, 1)  || * - * 1 * - *              ((5,3,1),2),   ((5,3,1),4,4), ((5,3,1),6)          
(5, 1, 2)  || * - * - * 1 *              ((5,1,2),2),   ((5,1,2),4),   ((5,1,2),6,6)         
(5, 2, 2)  || * 1 * - * 1 *              ((5,2,2),2,2), ((5,2,2),4),   ((5,2,2),6,6)          
(5, 3, 2)  || * - * 1 * 1 *              ((5,3,2),2),   ((5,3,2),4,4), ((5,3,2),6,6)          

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

[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.