Specializations and Symbolic Modeling

Abstract

We present the technique that allows splitting first-order logic formulae 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

-

The technique of symbolic verification of requirement specifications of software systems 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 determined 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 diagram 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 transformer” 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 satisfiability 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 ]. Workshops 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 performance. 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 performance 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 symbols: (i  0)  ( f (i)  f (0)) . After that we should apply basic protocol postcondition 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

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 environment state that depends on j, but not to whole environment state formula. In this example it could be j  0 only. If there are no predicates in projects ,which could compare values of attribute j with values of other attributes, then we could use some special 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 algorithm 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 protocol, 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 environment 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), the Ackermann reduction of the uninterpreted functional symbols is used, where attribute 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 substitution 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 considered 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 : t2  ...) 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, s2 ,...) consists of functional expressions which have external occurrences (not in arguments of such functional expressions) in formula part C of post-condition, but do not coincide with expressions from the set r. Finally, set z  (z1, z2 ,...) 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, considering 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) : t2 (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)  t2 (u,v, z))  ...) ,

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 qi corresponds to one of possible means of identification 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, k2 ,...),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  k2  l2  ...) . 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 independent 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)  Hi (z,u,v) where Hi (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 important 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 – attributes of model,  (x, a)  R(x, a)  C(x, a) , where R  (r1 : t1  r2 : t2  ...) is a conjunction of assignments and C is a formula part of postcondition, 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 conjunction 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)) .

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) : t2 (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))  q11  q21  ... , where qi1  (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))  (u2  t2 (r, s, z))  ...),u  {u1,u2 ,...} ,

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 identification. Formula Ei (u, v, z) is built in the same way as in forward predicate transformer [ 27 ]. 4

Specialization

4.1 Let We propose to use two types of specializations: 1. Specialization by memory usage 2. Specialization by functional symbol

Specialization by memory usage a1, a2 be sets of attributes from initial environment state a1  a2    a1  a2  a ,

S (a)  S1(a1)  S2 (a2 ) is environment B(x, a)  x(1(x1, a1)  2 (x2 , a2 )  P(x, a)  1(x1, a1)   2 (x2 , a2 )) is basic and state, protocol, where x1  x 2    x1  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

Proving.

Function sat builds closed formula. So, sat(S1(a1) 1(x1 , a1)  S2 (a2 )   2 (x 2 , a2 ))   sat(S1(a1) 1(x1 , a1))  sat(S2 (a2 )   2 (x 2 , a2 )) sat(S1(a1) 1(x1 , a1)  S2 (a2 )  2 (x 2 , a2 ))   (v1,v2 , x1, x2 )(S1(a1) 1(x1 , a1)  S2 (a2 )  2 (x 2 , a2 )) where v1,v2 are variables generated for attribute expression which depend on attributes a1, a2 .

It is known that a1  a2    a1  a2  a  x1  x 2    x1  x 2  x . It means that scope of quantifiers could be narrowed: (v1, v2 , x1, x2 )(S1(a1)  1(x1 , a1)  S2 (a2 )  2 (x 2 , a2 ))   (v1, x1)(S1(a1)  1(x1 , a1))  (v2 , x2 )(S2 (a2 )   2 (x 2 , a2 ))  i  sat(S1(a1)  1(x1 , a1))  sat(S2 (a2 )   2 (x 2 , a2 )) Theorem is proved.

This theorem means the following: 1. If S (a)  S1(a1)  S2 (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 satisfiability checking of S (a)   (x, a) . Checking of satisfiability of S2 (a2 ) is not required. 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( i Si (ai )  i (xi , ai ))   sat(Si (ai )   i (xi , ai )) . So, after if we say about such i pair of two sets a1i, ai2  ai  a1i  ai2    a1i  ai2  ai , then we understand that it 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(x1 , a1)  S2 (a2 )   2 (x 2 , a2 ),1(x1 , a1)   2 (x 2 , a2 ))   pt(S1(a1) 1(x1 , a1),1(x1 , a1))  pt(S2 (a2 )   2 (x 2 , a2 ), 2 (x 2 , a2 ))

Proving.

pt function builds sets r, s, z from postcondition 1(x1 , a1)   2 (x 2 , a2 ) and formula S1(a1) 1(x1 , a1)  S2 (a2 )   2 (x 2 , a2 ) , where r is a set of attribute expressions from left parts of assignments of postcondition, s is a set of attribute expressions 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(x1 , a1) , 1(x1 , a1) and S2 (a2 )   2 (x 2 , a2 ) ,  2 (x 2 , a2 ) are not intersected. It means that we could split each set r, s, z on

subsets r  r1  r2 ,s  s1  s2 ,z  z1  z2 and r1  r2   , s1  s2   , z1  z2   , because a1  a2  . Let’s write formula which is built by pt function.

Let

D(a,x)  D1(x1,a1)  D2(x2,a2),D1(x1,a1)  S1(a1) 1(x1,a1) , D2  S2(a2) 2(x2 ,a2) and 1(x1,a1)  R1(r1,s1,z1)  C1(r1,s1,z1),  2 (x2,a2)  R2(r2,s2,z2)  C2(r2,s2,z2) . So, general formula of predicate transC2(r2,s2,z2). because  (a,x)  1(x1,a1) 2(x2 ,a2).

Let’s write in details how to obtain iEi(u,v,z) . It is known that r1  r2   , s1  s2   , z1  z2   . 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;z2) . So, iEi(u,v,z)  (Ei1(u1,v1,z1))  ( Ei2 (u2,v2,z2))

i1 i2 Let’s consider formula of predicate transformer: pt(S1(a1) 1(x1,a1)  S2(a2) 1(x2 ,a2),1(x1,a1)  2(x2 ,a2))  iqi  (u,v)(D(u,v,z)  R(u,v,z)  (Ei(u,v,z))  C(r,s,z)) 

i  (u1,u2,u1,v2)(D1(u1,v1,z1)  D2(u1,v1,z1)   Ri(u1,v1,z1)  Ri(u2,v2,z2)   (Ei1(u1,v1,z1))  ( Ei2 (u2,v2,z2)) 

i1 i2  C1(r1,s1,z1)  C2(r2,s2,z2))   (u1,v1)(D1(u1,v1,z1)  R(u1,v1,z1)  (Ei1(u1,v1,z1)) 

i1  C1(r1,s1,z1))  (u2,v2)(D2(u2,v2,z2)  R(u2,v2,z2)   ( Ei2 (u2,v2,z2))  C2(r2,s2,z2)) ... 

i2  pt(D1(x1,a1),1(x1,a1))  pt(D2(x2 ,a2),2(x2 ,a2))

Theorem is proved.

4.4 Theorem 3

For backward mode it is true that: pt1(S1(a1)  C1(r1,s1,z1)  S2(a2)  C2(r2,s2,z2), 1(x1,a1) 2(x2 ,a2))  pt1(S1(a1)  C1(r1,s1,z1),1(x1,a1))  pt(S2(a2)  C2(r2,s2,z2),2(x2 ,a2))

Proving.

R(u,v,z)  R(u1,v1,z1)  R(u2,v2,z2) , C(r,s,z)  C1(r1,s1,z1)  C2(r2,s2,z2) because  (ra,x)  1(a1,x1) 2(a2,x2 ) . iEi(u,v,z)  (Ei1(u1,v1,z1))  i1 ( Ei2 (u2,v2,z2)) from previous theorem.

i2 pt-1(S(a)  C(r,s,z), (r,s,z))  iqi1   (u,v)(S(a)  C(r,s,z)  R(u,r,s,z)  Ei(u,v,z))  (r,s,z) 

i  (u1,u2,v1,v2)(S1(r1,s1,z1)  S2(r2,s2,z2)   C1(r1,s1,z1)  C2(r2,s2,z2)   (Ei1(u1,v1,z1))  ( Ei2 (u2,v2,z2))) 

i1 i2 1(r1,s1,z1) 2(r2,s2,z2)   (u1,v1)(S1(r1,s1,z1)  C1(r1,s1,z1)  (Ei1(u1,v1,z1))) 1(r1,s1,z1)  i1  (u2,v2)(S2(r2,s2,z2)  C2(r2,s2,z2)  ( Ei2 (u2,v2,z2))) 2(r2,s2,z2)  i2  pt1(S1(a1)  C1(r1,s1,z1),1(x1,a1))  pt(S2(a2)  C2(r2,s2,z2),2(x2 ,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) pt(S1(a1)1(x1,a1) S2(a2)2(x2 ,a2),1(x1,a1))   S2(a2)2(x2 ,a2) pt(S1(a1)1(x1,a1),1(x1,a1)) pt1(S1(a1)C1(r1,s1,z1)  S2(a2) C2(r2,s2,z2),1(x1,a1))   S2(a2)C2(r2,s2,z2)  pt1(S1(a1)C1(r1,s1,z1),1(x1,a1)) only, then

So, functions sat(Di(xi,ai)), pt(Di(xi,ai),i(xi,ai)) are called specialization, because we could use some special theories for implementation of it.

Examples of Usage of Specializations

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 postcondition 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. Application 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)  S2 (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    x1  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: ( 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, f2,...,v1,v2,a1,a2)  S1(a1)  S2(a2) be an environment state where f1  f2  ... are names of functional symbols, v1,v2 are variables for each functional attribute expression from sets a1,a2 correspondently, and

F( f1, f2,...,v1,v2,a1,a2)   ( f1 : v11  f1(t11,t12,...),v12  f1(t11,t12,...),..., f2 : v12  f2(t12,t22,...),v22  f22(t12,t22,...),...,...) where v11,v12 af1,v12,v22 af2 ,... are variables of type of functional names f1, f2,... for each attribute expression, afi is set of attribute, such as fi aj , 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, f2,...,v1,v2,a1,a2)  S1(a1)  S2(a2) . and b(a)  x(Fb( f1, f2,...,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(  (( fi(ti1,ti2,...)  fi(ti1,ti2,...))  (vik  vil))  (i,k,l)  S1(v1,a1) 1(v1,x1,a1)  S2(v2,a2) 2(v2,x2,a2))   sat(qi  Si(vi,ai) i(vi,ai,xi))

i where fi(ti1,ti2,...)  fi(ti1,ti2,...) is equality of arguments of functional attribute expressions.

Proving

Let’s define

F ( f1, f2 ,...,v1 ,v2 , a1, a2 , x1, x2 )  F ( f1, f2 ,...,v11,v12 , a1, a2 )   Fb ( f1, f2 ,...,v12 ,v22 , a1, a2 , x1, x2 ) . We combine all equations with the same name of from basic protocol. After that we obtain sets of variables v1 , v2 protocol b(a)  x(Fb ( f1, f 2 ,..., v1 , v2 , a1, a2 , x1, x2 ) 1(v1 , x1, a1) 

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  Si (vi, ai )   i(vi, ai , xi )) . i

Theorem is proved. 5.4

Theorem 5 where 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 ), S2 (v2 , a2 )  2 (v2 , x2 , a2 ), 2 (x2 , a2 )))) pt(Eij (vj , x j , a j ), S j (vj , a j )  j (vj , x j , a j ), j (x j , a j ))   qk , k qk  (u, v)(Si (u, v, z)  i (u, v, z)  R(u, v, z)   Eij (u, v, z)  Ek (u, v, z)  C(r, s, z) 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 disl 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. where 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 ), S2 (v2 , a2 )  C2 (v2 , x2 , a2 ), 2 (x2 , a2 )))) pt1(E ij (vj , x j , a j ), S j (vj , a j )  C j (vj , x j , a j ), j (x j , a j ))   qk , k qk (u, v)(S j (vj , a j )  C j (vj , x j , a j )  R(u, r, s, z)   Eij (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 specialized by concrete values is more than in 3 times. Of course, the speedup depends on 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 57%. 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 functions and functions with specialization are given.

Group of tests

Symbolic modeling is a powerful technique for the automated reachability of deadlocks and violations of user-defined properties. The main complexity of the reachability 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 provided and the correctness of such specializations is proved.

Specializations by memory usage and functional symbols are considered and examples for each are given.

The nearest plans are the investigation of additional kinds of specialization, because 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 Techniques . LNCS 1827 , pp. 311 - 328 . Springer Verlag, Berlin Heidelberg ( 1999 )

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 Requirements 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 Barcelogic 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 version) . Research report 4630 , LORIA ( 2002 )

15. Bozzano , M. , Bruttomesso , R. , Cimatti , A. , Junttila , T., van Rossum, P. , Schulz , S. , Sebastiani , 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 Encoding 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 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 Predicate 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 Algorithm 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 Transition Systems . Cybernetics and System Analysis , 4 , 91 - 99 ( 2010 )