Subject-Observer system for 1 subject

• A description of the Subject - Observer system was published in [1] and its CI model for one subject was 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.

• Modelling: 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: The control component (Subject) models four independent methods, update(), register(), deregister(), getValue(), and hence its model consists of four independent parallel parts. In the figure bellow, they are denoted as S₁, 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 methods register(), deregister(), getValue() (automata S₂, S₃, S₄), the Subject only receives the call and then returns. More interesting behaviour could be inserted on the place of state 2.

• A user component: Models that the Observer first 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.

• Numbers of states: The model of part S₁ has 5 sates, the other parts of the model has 2 sates, thus the whole control component model has 5*2*2*2 = 40 states and the model of user component has 7 states.

• CI model of the system with 8 users: Challange8.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
(1, 1, 1, 2)  || * - * - * 1 *  

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