Download Paper - STS

3 Model repair
which leads to the returned model (M 0 , s00 ). As (M 0 , s00 ) could be an invalid model for
φ1 , φ1 is a constraint for the repair of φ2 . This restricts the available repairs for φ2 to
those that also validate φ1 . As a consequence, there is always a set of constraints that
has be satisfied while repairing a model (which is not depicted in the update functions).
Listing 3.3: Model update: U pdateEU
f u n c t i o n U pdateEU ((M, s0 ), E[φ1 U φ2 ])
input
(M, s0 ) and E[φ1 U φ2 ] , where M = (S, R, L) , s0 ∈ S , and (M, s0 ) 6 E[φ1 U φ2 ] ;
output
(M 0 , s00 ) , where M 0 = (S 0 , R0 , L0 ) , s00 ∈ S 0 and (M 0 , s00 ) E[φ1 U φ2 ] ;
begin
i f (M, s0 ) 6 φ1 , then (M 0 , s00 ) = CTLUpdate ( (M, s0 ) , φ1 ) ;
e l s e do ( a ) o r ( b ) :
( a ) i f (M, s0 ) φ1 , and t h e r e i s a path π = [s∗ , ...] (s0 6= s∗ )
such t h a t (M, s∗ ) E[φ1 U φ2 ] ,
then a p p l y PU1 t o form a new model M 0 = (S 0 , R0 , L0 ) :
S 0 = S; R0 = R ∪ {(s0 , s∗ )}; ∀s ∈ S L0 (s) = L(s) ;
( b ) s e l e c t a path π = [s0 , ..., si , ..., sj , ...] ;
i f ∀s s0 < s < si , (M, s) φ1 , (M, sj ) φ2 ,
but ∀s0 si+1 < s0 < sj−1 , (M, s0 ) 6 φ1 ∨ φ2
then a p p l y PU1 t o form a new model M 0 = (S 0 , R0 , L0 ) :
S 0 = S; R0 = R ∪ {(si , sj )}; ∀s ∈ S , L0 (s) = L(s) ;
i f ∀s s < si , (M, s) φ1 , and ∀s0 s0 > si+1 , (M, s0 ) 6 φ1 ∨ φ2 ,
then a p p l y PU4 t o form a new model M 0 = (S 0 , R0 , L0 ) :
S 0 = S ∪ {s∗ }; R0 = R ∪ {(si−1 , s∗ ), (s∗ , si )} ;
∀s ∈ S , L0 (s) = L(s) , L(s∗ ) i s d e f i n e d such t h a t (M 0 , s∗ ) φ2 ;
i f (M 0 , s00 ) E[φ1 U φ2 ] , then return (M 0 , s00 ) ;
e l s e U pdateEU ((M 0 , s00 ), E[φ1 U φ2 ]) ;
end
Source: “CTL Model Update for System Modifications” [ZD10]
The last type of formulas are the ones with a temporal operator at the top level. An
exemplary update function is depicted in Listing 3.3. This is the one for the temporal
operator EU . The main difference between the previously presented update functions
and the ones for temporal operators is the reasoning about paths in the Kripke model.
This can be seen in the first else branch in Listing 3.3. U pdateEU tries to transform an
invalid path into a valid one to form an admissible model for the formula E[φ1 U φ2 ]. For
that, it chooses one of two repair strategies non-deterministically. The first strategy is
to connect the given state s0 to a state s∗ in the Kripke model where M, s∗ E[φ1 U φ2 ]
already holds. The second strategy is to take a path starting at s0 where φ1 holds in
the beginning up to a state si and where φ2 holds later at sj . The algorithm then adds
the transition (si , sj ) to R to jump over the states where neither φ1 nor φ2 hold. In
the case that no such state sj exists, U pdateEU introduces a new state s∗ with a label
that satisfies φ2 . s∗ is then inserted into the path between si−1 and si . As φ1 holds up
to si or si−1 and φ2 holds at sj or s∗ , M, s0 E[φ1 U φ2 ] should hold, too. If that is
not the case then U pdateEU tries to repair the current updated model (again). Since in
each repair step the number of available paths to choose from decreases, U pdateEU will
terminate eventually.
14