=Paper=
{{Paper
|id=None
|storemode=property
|title=Specializations and Symbolic Modeling
|pdfUrl=https://ceur-ws.org/Vol-1000/ICTERI-2013-p-490-505-SMSV.pdf
|volume=Vol-1000
|dblpUrl=https://dblp.org/rec/conf/icteri/PeschanenkoGS13
}}
==Specializations and Symbolic Modeling==
https://ceur-ws.org/Vol-1000/ICTERI-2013-p-490-505-SMSV.pdf
Specializations and Symbolic Modeling
Vladimir Peschanenko1, Anton Guba2 and Constantin Shushpanov3
1
Kherson State University, 27, 40 rokiv Zhovtnya str., Kherson, 73000 Ukraine,
vladimirius@gmail.com
2
Glushkov Institute of Cybernetics of NAS of Ukraine, 40, Glushkova ave., Kyiv, 03680,
antonguba@ukr.net
3
LLC «Information Software Systems», 15, Bozhenko str., Kyiv, 03680 Ukraine,
costa@iss.org.ua
Abstract. We present the technique that allows splitting first-order logic formu-
lae into parts which helps to use the special algorithms of satisfiability checking
and predicate transformer, which are the specializations. We describe the
mathematical description of the algorithm of the constructing specializations
and a few particular approaches to them, which speed up modeling of industrial
models. We prove the correctness of satisfiability and predicate transformer
functions. We consider forward and backward applicability of basic protocols
during symbolic modeling and verification We introduce the examples for each
specialization. We provide the experiments with typical real examples.
Keywords. Symbolic modeling, satisfiability, predicate transformer
Key terms. FormalMethod, MathematicalModeling, SoftwareComponent,
VerificationProcess
1 Introduction
The technique of symbolic verification of requirement specifications of software sys-
tems has shown good results in automatic detection of reachability of deadlocks and
violation of user-defined properties [1]. In previous works [2-4] symbolic models of
systems being transition systems with symbolic states represented by formulae of first
order logic were considered. A relation of transitions between the formulae is deter-
mined and marked by basic protocols, which are considered as actions, performed in
the system. A basic protocol is a formula of dynamic logic
x ( ( x, a ) P ( x, a ) ( x, a )) and it describes local properties of the system in
terms of pre- and postconditions α and β. Both are formulae of first order multisorted
logic interpreted on a data domain, P is a process, represented by means of MSC dia-
Specializations and Symbolic Modeling 491
gram and describes the reaction of a system triggered by the precondition, x is a set of
typed data variables, and a is a set of environment attributes. The general theory of
basic protocols is presented in [5].
A transition is considered as an operator in the space of postcondition formulae.
As the operator transforms one formula to another, in [6] a term “predicate trans-
former” is used. Thus, to compute transitions between the states of such models basic
protocols are interpreted as predicate transformers: for given symbolic state of the
system and given basic protocol the direct predicate transformer generates the next
symbolic state as its strongest postcondition, and the backward predicate transformer
generates the previous symbolic state as its weakest precondition. These concepts
have been implemented in VRS (Verification of Requirement Specifications) system
[7] and IMS (Insertion Modeling System) system [8].
An amount of papers with novel and very efficient techniques for computing satis-
fiability using SAT/SMT has been published in the last years, and some very efficient
SMT tools are now available (e.g., BarceLogic [9], CVCLite/CVC/CVC4 [10,11,12],
DLSAT [13], haRVey [14], MathSAT [15], SDSAT [16], TSAT++ [17], UCLID
[18], Yices [19], Verifun [20], Zapato [21], Z3 [22]). An amount of benchmarks,
mostly derived from verification problems, is available at the SMT-LIB [23]. Work-
shops devoted to SMT and official competitions on SMT tools are run yearly.
All these tools could be configured with the help of many parameters, which
means the usage of some techniques, tactics, heuristics or not, in order to gain in per-
formance. In the paper [24] the algorithm configuration problem is stated as follows:
given an algorithm, a set of parameters for the algorithm, and a set of input data,
found parameter values under which the algorithm achieves the best possible per-
formance on the input data. It gives a possibility of automated tuning of algorithm for
obtaining performance on formulae of some theory.
Usually during modeling of real projects we deal with complex environment states
and simple formulae of basic protocols (pre- and postconditions). It means that we
should check the satisfiability of the conjunction of the environment state and the
precondition formula and transform this whole big formula with the help of predicate
transformer [6]. Obviously, the manipulation with whole formulae is not required for
most of cases.
For example, let i, j : int, f : int int be attributes and f (i ) 0 f (0) 5
j 0 be an environment state, and 1 j : j 1 be a basic protocol. Let’s apply
this basic protocol to the environment state. First, the satisfiability of conjunction of
basic protocol precondition and environment state should be checked:
f (i ) 0 f (0) 5 j 0 . This checking should use the notion of functional sym-
bols: (i 0) ( f (i ) f (0)) . After that we should apply basic protocol postcondi-
tion to conjunction of environment state and precondition (see section Application of
Basic Protocol):
(v : int)( f (i ) 0 f (0) 5 v 0 ( j v 1))
f (i ) 0 f (0) 5 (v : int)(v 0 ( j v 1))
f (i ) 0 f (0) 5 j 1
492 V. Peschanenko, A. Guba and C. Shushpanov
It is known that basic protocol changes attribute j only (see section about predicate
transformers). It means that we could apply basic protocol to small part of environ-
ment state that depends on j, but not to whole environment state formula. In this ex-
ample it could be j 0 only. If there are no predicates in projects ,which could com-
pare values of attribute j with values of other attributes, then we could use some spe-
cial theories for manipulating with such formulae. In this example numeral intervals
could be used for representation of values of attribute j. We call such special theories
Specialization of sat, pt functions according to our general algorithm.
So, the main goal of this paper is to present a mathematical description of algo-
rithm of constructing specializations and a few particular approaches to specialization
which speed up modeling of industrial models. This paper is a continuation of the
[25], where only concrete values as a kind of specialization were described.
In the Section 2 we describe the process of forward application of a basic protocol
with the help of the satisfiability and the forward predicate transformer. In the Section
3 we present an applicability of basic protocols using satisfiability and backward
predicate transformer. The specializations by memory usage and functional symbols
are proposed in the Section 4. The results of experiments are discussed in the Section
5. In the Section 6 we summarize advantages of usage of the specializations and what
could be done in the nearest future.
2 Forward Application of Basic Protocol
Let S(a) be an environment state, x( ( x, a ) P ( x, a ) ( x, a )) be a basic proto-
col, where x – parameters of basic protocol, a – attributes of model,
D ( x, a ) E ( a ) ( x, a ) – conjunction of environment state and precondition of
basic protocol.
At the first step of application of basic protocol satisfiability of conjunction of en-
vironment state and precondition of basic protocol is checked: sat ( D ( x, a)) . If the
formula is unsatisfiable, then basic protocol is not applicable to environment state
S(a). If not, then process P ( x, a) is run and after forward predicate transformer is
applied: pt ( D ( x, a ), ( x, a )) . The process of P ( x, a) is not considered in the paper,
because the specialization tries to speed up the functions sat and pt.
2.1 Satisfiability
The checking formula satisfiability function sat is based on the Shostak method,
adapted to combination of numerical, symbolic and enumerated data types. If all of
the attribute expressions (simple attributes and functional symbols with parameters)
that are free in the formula S are simple, then for satisfiability checking it is sufficient
to prove validity of the closed formula (a, x) D ( x, a ) , where a is a set of all simple
attributes which occur in S, x is a set of parameters of basic protocol. For attribute
expressions with parameters (including access functions to the elements of arrays),
Specializations and Symbolic Modeling 493
the Ackermann reduction of the uninterpreted functional symbols is used, where at-
tribute expression is an attribute or functional symbol with parameters.
The Shostak method consists of the following. An expression of the form f (x) is
called as Functional Expression, if f is an attribute and x is a list of its parameters. At
first, superpositions of functional expressions are eliminated by successive substitu-
tion of every internal occurrence of f (x) by a new variable y, bounded by existential
quantifier and added to the formula y f (x ) . For example, formula P ( f ( g ( x))) is
replaced by formula y ( y g ( x) P ( f ( y ))) . After all such replacements there will
not be complex functional expressions in the formula. Further, for every attribute
expression f of functional type all its occurrences f ( x1 ),..., f ( xn ) with the different
parameters x1 ,..., xn are considered. Occurrence f ( xi ) is replaced by variable yi ,
bounded by existential quantifier and substitutive equations ( xi x j ) ( yi y j )
are added. Now in the formula there are only simple attributes, and a method consid-
ered in [26] is used.
2.2 Forward Predicate Transformer
In general case, the post-condition looks like ( x, a ) R ( x, a ) C ( x, a ) , where
R ( r1 : t1 r2 : t 2 ...) is a conjunction of assignments and C(x,a) is a formula
part of post-condition.
We will consider three sets of functional expressions (we consider attributes as a
functional expression with 0 arity): r, s and z. Set r (r1 , r2 ,...) consists of the left
parts of assignment, and also of other functional expressions that recursively depend
on the left parts. In other words, r consists of the left parts of assignments and, if
some functional expression f is included into this set, then all functional expressions
in which f occurs are also included in r. Set s ( s1 , s 2 ,...) consists of functional ex-
pressions which have external occurrences (not in arguments of such functional ex-
pressions) in formula part C of post-condition, but do not coincide with expressions
from the set r. Finally, set z ( z1 , z 2 ,...) consists of functional expressions which
have external occurrences in formula D in right parts of assignments and in internal
occurrences (in arguments if functional expressions) of the functional expressions of
formula part C of post-condition and left parts of assignments, but these assignments
are not included in two other sets (including parameter of basic protocol). Now, con-
sidering formulae, from which a post-condition and formula D are constructed as
functions of external occurrences of elements of these sets, we get a presentation of
post-condition in the following form:
B (r , s, z ) (r1 (r , s, z ) : t1 (r , s, z ) r2 (r , s, z ) : t 2 ( r , s, z ) ...) C ( r , s, z ) ,
Predicate transformer is determined by the following formula:
pt ( D (r , s, z ), (r , s, z )) q1 q2 ... ,where
qi (u , v )( D (u , v, z ) R (u , v, z ) Ei (u , v, z ) C ( r , s, z )) ,
R (u , v, z ) (r1 (u , v, z ) t1 (u , v, z )) (r2 (u , v, z ) t 2 (u , v, z )) ...) ,
494 V. Peschanenko, A. Guba and C. Shushpanov
Formula R (u , v, z ) is a quantifier-free part of the assignment formula. Set of the
variables u(v) represents new variables for each attribute expression from r(s) set. The
pt substitutes attributes from r(s) set to variables from u(v) set in corresponded part of
formula.
Each of disjunctive members q i corresponds to one of possible means of identifi-
cation of functional expressions occurring in formulae ( x, a ) , and Ei (u , v, z ) is a set
of equalities and inequalities corresponding to such identification.
To describe the construction of Ei (u , v, z ) we will consider the set M of all pairs
of functional expressions in the form ( f (k ), f (l )), k (k1 , k 2 ,...), l (l1 , l2 ,...) , where
f (k ) is chosen from set z, and f (l ) – from sets r and s. These functional expressions
shall be equal if their arguments were equal before application of basic protocol.
Let’s choose arbitrary subset N M (including an empty set for every pair
( f (k ), f (l )) N we will consider conjunction of equalities
k l , ( k1 l1 k 2 l 2 ...) . We will unite all such conjunctions in one and will add
to it conjunctive negations of all equalities, which correspond to pairs which are not
included into the set N. We will denote the obtained formula as Gi (r , s, z ) . If this
formula is satisfiable, then the choice is successful. Now obviously, f (k ) is not inde-
pendent and shall change the value because Gi (r , s, z ) is true. Thus, f (k ) shall
change the value in the same way as f (l ) . Set Ei (r , s, z ) Gi (r , s, z ) H i ( z , u , v)
where H i ( z , u , v ) is a conjunction of equalities f (k ) w if a variable w corresponds
to f (l ) . Thus, if f (k ) coincides with several functional expressions, it is not impor-
tant what variable is chosen (transitivity of equality) [6].
3 Backward Application of Basic Protocol
Let S (a ) be an environment state after the application of the basic protocol
x( ( x, a ) P ( x, a ) ( x, a )) , where x is parameters of basic protocol, a – attrib-
utes of model, ( x, a ) R ( x, a ) C ( x, a ) , where R (r1 : t1 r2 : t 2 ...) is a
conjunction of assignments and C is a formula part of post-
condition, D ( x, a ) S (a ) C ( x, a ) is a conjunction of environment state and formula
part of postcondition of basic protocol.
3.1 Satisfiability
At first step of application of basic protocol in backward mode satisfiability of con-
junction of environment state and formula part of postcondition of basic protocol is
checked: sat ( D( x, a )) . If the formula is unsatisfiable, then the basic protocol is not
applicable to environment state S (a ) .If not, then process P ( x, a ) is run and after a
backward predicate transformer is applied: pt 1 ( D ( x, a ), ( x, a )) .
Specializations and Symbolic Modeling 495
3.2 Backward Predicate Transformer
A backward predicate transformer considers three sets of functional expressions r, s
and z (as forward too). A postcondition of the basic protocols is represented by the
following formula:
B (r , s, z ) (r1 (r , s, z ) : t1 (r , s, z ) r2 (r , s, z ) : t 2 (r , s, z ) ...) C ( r , s, z )
A backward predicate transformer is determined by the following formula:
pt -1( D(r , s, z ), (r , s, z )) q11 q21 ... , where
qi1 (u, v)( D(u, v, z ) R(u, r , s, z ) Ei (u, v, z )) (r , s, z ) ,
R (u , r , s, z ) (u1 ( r , s, z ) t1 ( r , s, z )) (u 2 t 2 ( r , s, z )) ...), u {u1 , u 2 ,...} ,
Each of disjunctive members qi corresponds to one of possible identification of
functional expressions, occurring in formulae ( x, a ) and environment state S(a),
where Ei (u , v, z ) are sets of equalities and inequalities corresponding to such identifi-
cation. Formula Ei (u , v, z ) is built in the same way as in forward predicate trans-
former [27].
4 Specialization
We propose to use two types of specializations:
1. Specialization by memory usage
2. Specialization by functional symbol
4.1 Specialization by memory usage
Let a1,a2 be sets of attributes from initial environment state and
a1 a2 a1 a2 a , S (a) S1 (a1 ) S 2 (a2 ) is environment state,
B( x, a) x(1 ( x1 , a1 ) 2 ( x2 , a2 ) P( x, a) 1 ( x1, a1 ) 2 ( x2 , a2 )) is basic
protocol, where x1 x 2 x 1 x 2 x .
If B( x, a) x( i ( x, a) P( x, a) ( x, a)) then sat ( S (a) ( i ( x, a)))
i i
sat ( S (a ) i ( x, a )) and pt ( S (a) ( i ( x, a)), ( x, a)) pt ( S (a)
i i i
i ( x, a ), ( x, a )) . So, in the next text we consider basic protocol as B ( x, a ) only.
4.2 Theorem 1
sat ( S1 (a1 ) 1 ( x 1 , a1 ) S 2 (a2 ) 2 ( x 2 , a2 ))
sat ( S1 (a1 ) 1 ( x 1 , a1 )) sat ( S 2 (a2 ) 2 ( x 2 , a2 ))
Proving.
Function sat builds closed formula. So,
496 V. Peschanenko, A. Guba and C. Shushpanov
sat ( S1 (a1 ) 1 ( x 1 , a1 ) S 2 (a2 ) 2 ( x 2 , a2 ))
(v1 , v2 , x1 , x2 )( S1 (a1 ) 1 ( x 1 , a1 ) S 2 (a2 ) 2 ( x 2 , a2 ))
where v1 ,v2 are variables generated for attribute expression which depend on at-
tributes a1 , a2 . It is known that a1 a2 a1 a2 a x1 x 2
x 1 x 2 x . It means that scope of quantifiers could be narrowed:
(v1 , v2 , x1 , x2 )( S1 (a1 ) 1 ( x 1 , a1 ) S 2 (a2 ) 2 ( x 2 , a2 ))
(v1 , x1 )( S1 (a1 ) 1 ( x 1 , a1 )) (v2 , x2 )( S 2 (a2 ) 2 ( x 2 , a2 )) i
sat ( S1 (a1 ) 1 ( x 1 , a1 )) sat ( S 2 (a2 ) 2 ( x 2 , a2 ))
Theorem is proved.
This theorem means the following:
1. If S (a ) S1 (a1 ) S 2 (a2 ) and (a, x) 1 ( x1 , a1 ) and S (a ) is satisfiable, then it
is enough to check satisfiability of conjunction of S1 (a1 ) 1 ( x1 , a1 ) for satisfi-
ability checking of S (a ) ( x, a ) . Checking of satisfiability of S 2 (a2 ) is not re-
quired.
2. Checking of each part sat ( Si (ai ) i ( xi , ai )) could be done concurrently.
This case could be easily generalized to a1 ,...., an case, because if it is possible to
build subsets a1i , ai2 ai a1i ai2 a1i ai2 ai and to spilt an environment
state and basic protocol accordingly to the theorem 1, then
sat ( Si (ai ) i ( xi , ai )) sat ( Si (ai ) i ( xi , ai )) . So, after if we say about such
i i
pair of two sets ai , ai ai a1i ai2 a1i ai2 ai , then we understand that it
1 2
could be applicable and for n sets.
Let’s see how forward and backward predicate transformer can be applied.
4.3 Theorem 2
For forward application of basic protocol it is true that:
pt ( S1 (a1 ) 1 ( x 1 , a1 ) S 2 (a2 ) 2 ( x 2 , a2 ), 1 ( x 1 , a1 ) 2 ( x 2 , a2 ))
pt ( S1 (a1 ) 1 ( x 1 , a1 ), 1 ( x 1 , a1 )) pt ( S 2 (a2 ) 2 ( x 2 , a2 ), 2 ( x 2 , a2 ))
Proving.
pt function builds sets r , s , z from postcondition 1 ( x 1 , a1 ) 2 ( x 2 , a2 ) and
formula S1 (a1 ) 1 ( x 1 , a1 ) S 2 (a2 ) 2 ( x 2 , a2 ) , where r is a set of attribute ex-
pressions from left parts of assignments of postcondition, s is a set of attribute ex-
pressions from formula part of postcondition, z is a set of other attribute expressions
from formula and postcondition. We know that sets of attribute expressions from pairs
S1 (a1 ) 1 ( x 1 , a1 ) , 1 ( x 1 , a1 ) and S 2 (a2 ) 2 ( x 2 , a2 ) , 2 ( x 2 , a2 ) are not inter-
sected. It means that we could split each set r , s, z on subsets
Specializations and Symbolic Modeling 497
r r1 r 2 , s s 1 s 2 , z z 1 z 2 and r1 r2 , s1 s 2 ,
z 1 z 2 , because a1 a2 . Let’s write formula which is built by pt func-
tion.
Let D(a, x) D1 ( x1 , a1 ) D2 ( x2 , a2 ), D1 ( x 1 , a1 ) S1 (a1 ) 1 ( x 1 , a1 ) ,
D 2 S 2 (a2 ) 2 ( x 2 , a2 ) and 1 ( x 1 , a1 ) R1 (r1 , s1 , z1 ) C1 (r1 , s1 , z1 ) ,
2 ( x2 , a2 ) R2 (r2 , s2 , z 2 ) C2 (r2 , s2 , z 2 ) . So, general formula of predicate trans-
former is the following:
qi (u, v)( D(u , v, z ) R(u, v, z ) ( Ei (u , v, z )) C (r , s, z ))
i i
where R (u , v, z ) R1 (u1 , v1 , z1 ) R2 (u 2 , v2 , z 2 ) , C (r , s, z ) C1 (r1 , s1 , z1 )
C 2 ( r2 , s2 , z 2 ). because (a, x) 1 ( x 1 , a1 ) 2 ( x 2 , a2 ) .
Let’s write in details how to obtain Ei (u , v, z ) . It is known that r1 r 2 ,
i
s 1 s 2 , z 1 z 2 . To build such disjunction we should take into account
all pairs of functional attribute expressions from sets r,s and z. It means that each such
pair should be in set of attribute (r1 s1; z1 ) or (r2 s2 ; z 2 ) . So,
Ei (u , v, z ) ( Ei1 (u1 , v1 , z1 )) ( Ei2 (u 2 , v2 , z 2 ))
i i1 i2
Let’s consider formula of predicate transformer:
pt ( S1 (a1 ) 1 ( x 1 , a1 ) S 2 (a2 ) 1 ( x 2 , a2 ), 1 ( x 1 , a1 ) 2 ( x 2 , a2 ))
qi (u , v)( D(u , v, z ) R (u, v, z ) ( Ei (u , v, z )) C (r , s, z ))
i i
(u1 , u 2 , u1 , v2 )( D1 (u1 , v1 , z1 ) D2 (u1 , v1 , z1 )
Ri (u1 , v1 , z1 ) Ri (u 2 , v2 , z 2 )
( Ei1 (u1 , v1 , z1 )) ( Ei2 (u 2 , v2 , z 2 ))
i1 i2
C1 (r1 , s1 , z1 ) C2 (r2 , s2 , z 2 ))
(u1 , v1 )( D1 (u1 , v1 , z1 ) R(u1 , v1 , z1 ) ( Ei1 (u1 , v1 , z1 ))
i1
C1 (r1 , s1 , z1 )) (u 2 , v2 )( D2 (u 2 , v2 , z 2 ) R(u 2 , v2 , z 2 )
( Ei2 (u 2 , v2 , z 2 )) C2 (r2 , s2 , z 2 )) ...
i2
pt ( D1 ( x 1 , a1 ), 1 ( x 1 , a1 )) pt ( D2 ( x 2 , a2 ), 2 ( x 2 , a2 ))
Theorem is proved.
4.4 Theorem 3
For backward mode it is true that:
498 V. Peschanenko, A. Guba and C. Shushpanov
pt 1 ( S1 (a1 ) C1 (r1 , s1 , z1 ) S 2 (a2 ) C2 (r2 , s2 , z 2 ),
1 ( x 1 , a1 ) 2 ( x 2 , a2 )) pt 1 ( S1 (a1 ) C1 (r1 , s1 , z1 ), 1 ( x 1 , a1 ))
pt ( S 2 (a2 ) C2 (r2 , s2 , z 2 ), 2 ( x 2 , a2 ))
Proving.
R (u , v, z ) R (u1 , v1 , z1 ) R (u 2 , v2 , z 2 ) , C ( r , s, z ) C1 ( r1 , s1 , z1 ) C2 ( r2 , s2 , z 2 )
because (ra , x) 1 (a1 , x 1 ) 2 (a2 , x 2 ) . Ei (u, v, z ) ( Ei1 (u1 , v1 , z1 ))
i i1
( Ei2 (u 2 , v2 , z 2 )) from previous theorem.
i2
pt -1 ( S (a) C (r , s, z ), (r , s, z )) qi1
i
(u , v)( S (a ) C (r , s, z ) R(u , r , s, z ) Ei (u , v, z )) (r , s, z )
i
(u1 , u 2 , v1 , v2 )( S1 (r1 , s1 , z1 ) S 2 (r2 , s2 , z 2 )
C1 (r1 , s1 , z1 ) C2 (r2 , s2 , z 2 )
( Ei1 (u1 , v1 , z1 )) ( Ei2 (u 2 , v2 , z 2 )))
i1 i2
1 (r1 , s1 , z1 ) 2 (r2 , s2 , z 2 )
(u1 , v1 )( S1 (r1 , s1 , z1 ) C1 (r1 , s1 , z1 ) ( Ei1 (u1 , v1 , z1 ))) 1 (r1 , s1 , z1 )
i1
(u 2 , v2 )( S 2 (r2 , s2 , z 2 ) C2 (r2 , s2 , z 2 ) ( Ei2 (u 2 , v2 , z 2 ))) 2 (r2 , s2 , z 2 )
i2
1
pt ( S1 (a1 ) C1 (r1 , s1 , z1 ), 1 ( x 1 , a1 )) pt ( S 2 (a2 ) C2 (r2 , s2 , z 2 ), 2 ( x 2 , a2 ))
Theorem is proved.
Theorem 2 and theorem 3 mean that:
1. Functions pt, pt-1 could be applied separately and concurrently.
2. If postcondition contains 1 ( x1 , a1 ) only, then
pt ( S1 (a1 ) 1 ( x 1 , a1 ) S 2 (a2 ) 2 ( x 2 , a2 ), 1 ( x 1 , a1 ))
S 2 (a2 ) 2 ( x 2 , a2 ) pt ( S1 (a1 ) 1 ( x 1 , a1 ), 1 ( x 1 , a1 ))
pt 1 ( S1 (a1 ) C1 (r1 , s1 , z1 ) S 2 (a2 ) C2 (r2 , s 2 , z 2 ), 1 ( x 1 , a1 ))
S 2 (a2 ) C 2 (r2 , s 2 , z 2 ) pt 1 ( S1 (a1 ) C1 (r1 , s1 , z1 ), 1 ( x 1 , a1 ))
So, functions sat ( Di ( xi , ai )), pt ( Di ( xi , ai ), i ( xi , ai )) are called specialization, be-
cause we could use some special theories for implementation of it.
Specializations and Symbolic Modeling 499
5 Examples of Usage of Specializations
5.1 Examples of Specializations by Memory Usage
Example 1. Concrete values. Let S (a ) (i 2) S (a / i ) be an environment state
where i : int and a / i is a set of all attributes in model except i,
b x((i 0) (i : i 1)) . For application of such basic protocol we should
check satisfiability of the next formula: sat ((i 2) (i 0)) 1 , and the postcondi-
tion should be applied to (i 2) : v((v 2) (v 0) (i v 1)) (i 3) . For such
examples direct C++ translation could be used instead of using some special theories,
and it will work much faster because it doesn’t require any additional checking, just
direct translation into C++ code and compilation of it.
Example 2. Let S (a ) (i 2) S (a / i ) be environment state where i : int and
a / i is a set of all attributes in model except i, b x((i 0) (i : i 1)) . For
application of such basic protocol we should check satisfiability of the next formula:
sat ((i 2) (i 0)) 1 , and the postcondition should be applied to (i 2) :
v((v 2) (v 0) (i v 1)) (i 1) (i 3) . For such examples numerical
intervals could be used. So, S (a ) (i (;2)) S (a / i ) ,
b x((i (0;)) (i : i 1)) . Satisfiability checking looks like just crossing of
two numerical intervals: i (;2) (0;) i (0;2) i [1;1] for integer. Appli-
cation of pt creates the following formula: v((v [1;1]) (i v 1))
i 1 [1;1] i [2;2] . This approach will work faster than general satisfiability
checking and quantifiers eliminations. Such approach could be used for all numeric
and enumerated types.
5.2 Examples of Specializations by Functional Symbol
It is not always possible to represent environment state and basic protocols in the
following way: S (a) S1 (a1 ) S 2 (a2 ) , and B(a, x) x(1 ( x1 , a1 )
2 ( x2 , a2 ) P( x, a) 1 ( x1 , a1 ) 2 ( x2 , a2 ))
where a1 a2 ,
a1 a2 a , x1 x 2 x 1 x 2 x . One of such situation occurs when a value
of functional attribute expression and its parameter has different types and belongs to
the different subsets ai . For example, if functional attribute: i, j : int, f : int T is
defined where T (c1, c2 , c3 ) is enumerated type with three enumerated constants:
c1 , c2 , c3 , then formula ( f (i) c1 ) i 0 could be represented with specializations
as follows: ( f : v1 f (i)) (v1 c1 ) (i 0) . Let b 1 ( f ( j ) : c2 ) be a basic
protocol. Its specialized representation is: b 1 ( f : v1 f ( j )) (v1 : c2 ) 1 .
It is required to merge such data structures for pt function which should consider all
pairs of functional attribute expression from sets r,s and z:
500 V. Peschanenko, A. Guba and C. Shushpanov
( f : v1 f (i )) ( f : v1 f ( j )) ( f : v1 f (i ), v2 f ( j )) . After that basic protocol
should be transformed in the following form:
b 1 ( f : v2 f ( j )) (v2 : c2 ) 1 . It is required to take into account two
possible combinations: (i j ) (i j ) . So, we obtain:
pt (( f : v1 f (i ), v2 f ( j )) (v1 c1 ) i 0, v2 : c2 )
( f : v1 f (i ), v2 f ( j ))
v ((i j ) (v c1 ) (v2 c2 ))
v ((i j ) (v1 c1 ) (v2 c2 )) i 0
( f : v1 f (i ), v2 f ( j )) (v2 c2 ) i 0 (i j )
( f : v1 f (i ), v2 f ( j )) (v1 c1 ) (v2 c2 ) i 0 (i j )
( f : v1 f (i )) (v1 c2 ) i 0 (i j )
( f : v1 f (i ), v2 f ( j )) (v1 c1 ) (v2 c2 ) i 0 (i j )
Let S (a) F ( f1 , f 2 ,..., v1 , v2 , a1 , a2 ) S1 (a1 ) S 2 (a2 ) be an environment state
where f1 f 2 ... are names of functional symbols, v1, v2 are variables for each
functional attribute expression from sets a1 ,a2 correspondently, and
F ( f1 , f 2 ,..., v1 , v2 , a1 , a2 )
( f1 : v11 f1 (t11 , t12 ,...), v12 f1 (t11 , t12 ,...),...,
f 2 : v12 f 2 (t12 , t 22 ,...), v22 f 22 (t12 , t 22 ,...),...,...)
where v11 , v12 a f1 , v12 , v22 a f 2 ,... are variables of type of functional names
f1 , f 2 ,... for each attribute expression, a fi is set of attribute, such as fi a j ,
tij aii {ai } , … - corresponded arguments for each functional with the same name
are in one specialization, and Shostak’s method could be applied for each right part of
equation in F.
Let S (a) F ( f1 , f 2 ,..., v1 , v2 , a1 , a2 ) S1 (a1 ) S 2 (a2 ) . and
b(a) x( Fb ( f1 , f 2 ,..., v1 , v2 , a1 , a2 , x1 , x2 ) 1 (v1 , x1 , a1 )
2 (v2 , x2 , a2 ) P(a, x) 1 (v1.x1 , a1 ) 2 (v2 , x2 , a2 ))
5.3 Theorem 4
sat ( S (a) ( x, a)) sat ( (( f i (ti1 , ti2 ,...) f i (ti1, ti 2 ,...)) (vi k vil ))
(i , k , l )
S1 (v1 , a1 ) 1 (v1 , x1, a1 ) S 2 (v2 , a2 ) 2 (v2 , x2 , a2 ))
sat (qi Si (vi , ai ) i (vi , ai , xi ))
i
where f i (ti1 , ti2 ,...) f i (ti1 , ti 2 ,...) is equality of arguments of functional attribute
expressions.
Proving
Specializations and Symbolic Modeling 501
Let’s define F ( f1 , f 2 ,..., v1 , v2 , a1 , a2 , x1 , x2 ) F ( f1 , f 2 ,..., v11 , v12 , a1 , a2 )
Fb ( f1 , f 2 ,..., v12 , v22 , a1 , a2 , x1 , x2 ) . We combine all equations with the same name of
functional symbol f i and renaming variables names after such union for equations
from basic protocol. After that we obtain sets of variables v1 , v 2 and new basic
proto-
col b(a) x( Fb ( f1 , f 2 ,..., v1 , v 2 , a1 , a 2 , x1 , x 2 ) 1 (v1 , x1 , a1 )
2 (v2 , x2 , a2 ) ... P(a, x) 1 (v1 , x1 , a1 ) 2 (v2 , x2 , a2 )) .
For satisfiable checking we should add corresponded implication for each pair of
equation from F ( f1 , f 2 ,..., v1 , v2 , a1 , a2 , x1 , x2 ) with the same name of functional
symbol f i .
(( f i (ti1 , ti2 ,...) f il (ti1 , ti 2 ,...)) (vi k vil ))
(i , k , l )
(( f i (ti1 , ti2 ,...) f i (ti1 , ti 2 ,...)) (vi k vil ))
i, k , l
Each left and right parts of equation and negation of equations are in the same
specialization. It means that we could build here a disjunction of conjunction. Each
conjunct in such disjunction is qi which will be in one form of our specialization. So,
it means that we could check satisfiability in the following form
sat (qi S i (vi , ai ) i (vi , ai , xi )) .
i
Theorem is proved.
5.4 Theorem 5
pt ( S (a) ( x, a), ( x, a))
( pt ( E1i (v1 , x1 , a1 ), S1 (v1 , a1 ) 1 (v1 , x1 , a1 ), 1 ( x1 , a1 )))
i
pt ( E2i (v2 , x2 , a2 ), S 2 (v2 , a2 ) 2 (v2 , x2 , a2 ), 2 ( x2 , a2 ))))
where
pt ( E ij (vj , x j , a j ), S j (vj , a j ) j (vj , x j , a j ), j ( x j , a j )) qk ,
k
qk (u, v)( S i (u, v, z ) i (u, v, z ) R(u , v, z )
Ei j (u, v, z ) E k (u , v, z ) C (r , s, z )
Proving.
The sets v1 , v 2 are built in the same way as in theorem 3. Let’s consider a general
formula of predicate transformer:
pt ( D(r , s, z ), (r , s, z )) (u , v)( D(u , v, z ) R (u , v, z ) Ei (u , v, z ) C (r , s, z ) .
i
Coefficient Ei (u , v, z ) looks like disjunction of conjunction of all possible
i
matchings with functional attribute expressions from sets r,s and z. So, we can present
502 V. Peschanenko, A. Guba and C. Shushpanov
it as conjunction of two disjunctions: Ei (u , v, z ) ( Ek (u, v, z )) ( El (u, v, z ))
i k l
where Ek (u, v, z ) is disjunction for matching of functional attribute expression
k
where parameters and its value are from different sets of a j . El (u , v, z ) is a dis-
l
junction of matching of other functional attribute expression. Each conjunct of such
disjunction could be considered as a conjunction which depends on different sets of
memory a j . It means that disjunction of conjunction Ek (u, v, z ) could be prepared
k
early before calling of some pt function without corresponded substitution of x,y. So,
Ek (u , v, z ) E1k (v1 , x1 , a1 ) E2k (v2 , x2 , a2 ) . Disjunction El (u , v, z ) could be
k k l
presented in the same way. So, the theorem is proved.
5.5 Theorem 6
pt 1 ( S (a) C (r , s, z ), ( x, a))
( pt 1 ( E1i (v1 , x1 , a1 ), S1 (v1 , a1 ) C1 (v1 , x1 , a1 ), 1 ( x1 , a1 )))
i
pt 1 ( E2i (v2 , x2 , a2 ), S 2 (v2 , a2 ) C2 (v2 , x2 , a2 ), 2 ( x2 , a2 ))))
where
pt 1 ( E ij (vj , x j , a j ), S j (vj , a j ) C j (vj , x j , a j ), j ( x j , a j )) qk ,
k
qk (u, v)( S j (vj , a j ) C j (vj , x j , a j ) R (u , r , s, z )
Ei j (u , v, z ) Ek (u, v, z )) j (r , s, z )
This theorem could be proved in the same mode as theorem 4.
6 Experiments
In this section we present some results from our test suites. All experiments are
devided into several groups. We compare the time of modeling of the satisfiability
and the predicate transformer, presented in the Section 2, and these algorithms with
the specializations.
The first group of experiments refers to specialization by memory usage. Projects
contain formulae in which some attributes have only concrete values. Let us present
one typical real example. This example has a functional attribute of symbolic type
with integer parameters, simple enumerated and simple integer attributes. All of these
integer attributes initialize with concrete values and have concrete values at all times
during trace generation (basic protocols do not change those to symbolic ones). Other
attributes are symbolic. We provide a specialization for attributes, which are always
concrete. The difference of modeling time for this example and for this one special-
ized by concrete values is more than in 3 times. Of course, the speedup depends on
Specializations and Symbolic Modeling 503
project: more concrete attributes we have, more speedup we shall obtain. In [25] it
was shown that speedup could be in thousands times.
The second group of experiments refers also to specialization by memory usage,
but not to concrete values. Examples from this group have enumerated attributes and
integer attributes. Some of the integer attributes memories are intersected, some of
them are independent. First of all, we provide the splitting of formulae into two parts
according to attribute types: enumerated part and integer part. For the enumerated part
we use bitsets, for integer – common Pressburger algorithm. Speedup was about 5-
7%. After we specialize an integer part. We consider the attributes which memory is
independent and obtain speedup in 10 times.
So, the results of comparison of modeling time using general satisfiability func-
tions and functions with specialization are given.
Table 6. Results of experiments
Group of tests General With specializations
algorithm
1 930 sec 300 sec (memory usage/concrete values)
2 300 sec 280 sec (splitting by types)
3 300 sec 33 sec (memory usage/independent memory)
7 Conclusions
Symbolic modeling is a powerful technique for the automated reachability of dead-
locks and violations of user-defined properties. The main complexity of the reachabil-
ity problem is in the complexity of satisfiability and predicate transformer functions.
There are a lot of SMT-based techniques which speed up the satisfiability of formulae
that satisfy some particular theory. We propose a technique that allows to speedup
classical symbolic modeling when formulae could be splitted in several parts and used
some special theories for manipulations with them, which are called specializations.
The mathematical description of the algorithm for constructing specializations is pro-
vided and the correctness of such specializations is proved.
Specializations by memory usage and functional symbols are considered and ex-
amples for each are given.
The nearest plans are the investigation of additional kinds of specialization, be-
cause the more specializations we have, the more speedup we obtain.
References
1. Symbolic Modeling, http://en.wikipedia.org/wiki/Model_checking
2. Letichevsky, A., Gilbert, D.: A Model for Interaction of Agents and Environments. In:
Bert, D., Choppy, C., Moses, P. (eds.) Recent Trends in Algebraic Development Tech-
niques. LNCS 1827, pp. 311–328. Springer Verlag, Berlin Heidelberg (1999)
504 V. Peschanenko, A. Guba and C. Shushpanov
3. Letichevsky, A.: Algebra of Behavior Transformations and its Applications. In:
Kudryavtsev, V. B., Rosenberg, I. G. (eds.) Structural Theory of Automata, Semigroups,
and Universal Algebra, NATO Science Series II. Mathematics, Physics and Chemistry,
vol. 207, pp. 241–272. Springer Verlag, Berlin Heidelberg (2005)
4. Letichevsky A., Kapitonova J., Kotlyarov V., Letichevsky Jr., A., Nikitchenko N., Volkov,
V., Weigert T.: Insertion Modeling in Distributed System Design. Problems of
Programming, (4), 13–39 (2008)
5. Letichevsky, A., Kapitonova, J., Volkov, V., Letichevsky Jr., A., Baranov, S., Kotlyarov,
V., Weigert, T.: System Specification with Basic Protocols. Cybernetics and System
Analysis, (4), 3–21 (2005)
6. Letichevsky, A. A., Godlevsky, A. B., Letichevsky Jr., A. A., Potienko, S. V.,
Peschanenko, V. S.: Properties of Predicate Transformer of VRS System. Cybernetics and
System Analyses, (4), 3–16 ( 2010)
7. Letichevsky, A., Kapitonova, J., Letichevsky Jr., A., Volkov, V., Baranov, S., Kotlyarov,
V., Weigert, T.: Basic Protocols, Message Sequence Charts, and the Verification of Re-
quirements Specifications, In: ISSRE 2004, WITUL (Workshop on Integrated reliability
with Telecommunications and UML Languages) , Rennes, 4 November (2005)
8. Letichevsky, A., Letychevskyi, O., Peschanenko, V.: Insertion Modeling System. In:
Clarke, E.M., Virbitskaite, I., Voronkov, A. (eds.) PSI 2011. LNCS 7162, pp. 262–274,
Springer Verlag, Berlin Heidelberg (2011)
9. Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: The Barce-
logic SMT Solver. In: Gupta, Aarti and Malik, Sharad (eds.) CAV 2008. LNCS 5123, pp.
294–298, Springer Verlag, Berlin Heidelberg (2008)
10. Barrett, C., Berezin, S.: CVC Lite: A New Implementation of the Cooperating Validity
Checker. In: Rajeev, A., Peled, D.A. (eds.) CAV '04. LNCS 3114, pp. 515–518, Springer
Verlag, Berlin Heidelberg (2004)
11. Barrett, C., Tinelli, C.: CVC3. In: W. Damm and H. Hermanns (eds.) CAV '07. LNCS
4590, pp. 298–302, Springer Verlag, Berlin Heidelberg (2007)
12. Barrett, C., Conway, C. L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds,
A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV’11. LNCS 6806,
pp. 171–177, Springer Verlag, Berlin Heidelberg (2011)
13. Cotton, S., Asarin, E., Maler, O., Niebert, P.: Some Progress in Satisfiability Checking for
Difference Logic. In: Proc. FORMATS-FTRTFT (2004)
14. Déharbe, D., Ranise, S.: Bdd-Driven First-Order Satisfiability Procedures (extended ver-
sion). Research report 4630, LORIA (2002)
15. Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebas-
tiani, R.: An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic
Logic. In: Halbwachs, Lenore (eds.) TACAS’05. LNCS 3440, pp. 317–333, Springer
Verlag, Berlin Heidelberg (2005)
16. Ganai, M. K., Talupur, M., Gupta, A.: SDSAT: Tight Integration of Small Domain Encod-
ing and Lazy Approaches in a Separation Logic Solver. In: H. Hermanns, J. Palsberg.
(eds.) TACAS 2006. LNCS 3920, pp. 135–150. Springer Verlag, Berlin Heidelberg (2006)
17. Audemard, G., Bertoli, P. G., Cimatti, A., Kornilowicz, A., Sebastiani, R.: A SAT based
Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. In:
A. Voronkov (ed.) CADE 2002. LNCS (LNAI) 2392, pp. 195–210. Springer Verlag,
Berlin Heidelberg (2002)
18. Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and Verifying Systems using a Logic of
Counter Arithmetic with Lambda Expressions and Uninterpreted Functions.. In: Brinksma
Specializations and Symbolic Modeling 505
K., Larsen G. (eds) CAV’04. LNCS 2404, pp. 78–92, Springer Verlag, Berlin Heidelberg
(2002)
19. Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In T. Ball and
R.B. Jones, (eds.) CAV’06. LNCS 4144, pp. 81–94, Springer Verlag, Berlin Heidelberg
(2006)
20. Walther, C., Schweitzer, S.: About veriFun. In: F. Baader (eds.) CADE’03. LNCS 2741,
pp. 322–327, Springer Verlag, Berlin Heidelberg (2003)
21. Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: Automatic Theorem Proving for Predi-
cate Abstraction Refinement. In: Alur, R. A., Peled D. A. (eds.) CAV'04. LNCS 3114, pp.
457–461. Springer Verlag, Berlin Heidelberg (2004)
22. de Moura, L., Bjørner, N.: Z3: An Eficient SMT Solver. In: C. R. Ramakrishnan, J. Rehof
(eds.) TACAS'08, LNCS 4963, pp. 337–340. Springer Verlag, Berlin Heidelberg (2004)
23. Barrett, C., de Moura, L., Ranise, S., Stump, A., Tinelli, C.: The SMT-LIB Initiative and
the Rise of SMT. In: Barner S., Harris I. (eds.) HVC 2010. LNCS 6504, pp. 3–3, Springer
Verlag, Berlin Heidelberg (2010)
24. Hutter, F., Hoos, H.H., Leyton-Brown, K., Stuetzle, T.: ParamILS: an Automatic Algo-
rithm Configuration Framework. JAIR, 36, 267–306 (2009)
25. Peschanenko, V. S., Guba, А. А., Shushpanov, C. I.: Mixed Concrete-Symbolic Predicate
Transformer. Bulletin of Taras Shevchenko National University of Kyiv, Series Physics &
Mathematics, 2 (2013) (in press)
26. Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability Modulo Theories. Frontiers
in Artificial Intelligence and Applications, 185, 825–885 (2009)
27. Godlevsky, A. B.: Predicate Transformers in the Context of Symbolic Modeling of Transi-
tion Systems. Cybernetics and System Analysis, 4, 91–99 ( 2010)