Satisfiability For Symbolic Verification in VRS
Рассмотрены использование логики первого порядка в символьной верификации спецификаций требований программного обеспечения, символьные модели систем, которые есть транзиционными системами с символьными состояниями представленных формулой логики первого порядка. Использованы методы Satisfiability Mod...
Gespeichert in:
| Veröffentlicht in: | Управляющие системы и машины |
|---|---|
| Datum: | 2013 |
| Hauptverfasser: | , , , |
| Format: | Artikel |
| Sprache: | Englisch |
| Veröffentlicht: |
Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України
2013
|
| Schlagworte: | |
| Online Zugang: | https://nasplib.isofts.kiev.ua/handle/123456789/83170 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Zitieren: | Satisfiability For Symbolic Verification in VRS / A. Letichevsky, A. Letichevskyi, T. Weigert, V. Peschanenko // Управляющие системы и машины. — 2013. — № 3. — С. 81-87. — Бібліогр.: 26 назв. — англ. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1860147669253488640 |
|---|---|
| author | Letichevsky, A. Letichevskyi, A. Weigert, T. Peschanenko, V. |
| author_facet | Letichevsky, A. Letichevskyi, A. Weigert, T. Peschanenko, V. |
| citation_txt | Satisfiability For Symbolic Verification in VRS / A. Letichevsky, A. Letichevskyi, T. Weigert, V. Peschanenko // Управляющие системы и машины. — 2013. — № 3. — С. 81-87. — Бібліогр.: 26 назв. — англ. |
| collection | DSpace DC |
| container_title | Управляющие системы и машины |
| description | Рассмотрены использование логики первого порядка в символьной верификации спецификаций требований программного обеспечения, символьные модели систем, которые есть транзиционными системами с символьными состояниями представленных формулой логики первого порядка. Использованы методы Satisfiability Modulo Theory вместо логического вывода в соответствующем исчислении для эффективных вычислений в предикатных трансформерах.
This paper demonstrates the use of the first order logic in symbolic verification of the requirement specifications of reactive software systems. We consider symbolic models of a specified system which are transition systems with symbolic states represented by formulae of the first order logic. To efficiently compute predicate transformers the Satisfiability Modulo Theory methods are used instead of the logical inference in the corresponding calculi.
Розглянуто використання логіки першого порядку у символьній верифікації специфікацій вимог програмного забезпечення, символьні моделі систем, які є транзиційними системами з символьними станами представленими формулою логіки першого порядку. Використано методи Satisfiability Modulo Theory замість логічного виводу у відповідних численнях для ефективного обчислення у предикатних трансформерах.
|
| first_indexed | 2025-12-07T17:50:43Z |
| format | Article |
| fulltext |
УСиМ, 2013, № 3 81
UDC 519.686.2
A. Letichevsky, A. Letichevskyi, T. Weigert, V. Peschanenko
Satisfiability For Symbolic Verification in VRS
Рассмотрены использование логики первого порядка в символьной верификации спецификаций требований программного
обеспечения, символьные модели систем, которые есть транзиционными системами с символьными состояниями представ-
ленных формулой логики первого порядка. Использованы методы Satisfiability Modulo Theory вместо логического вывода в
соответствующем исчислении для эффективных вычислений в предикатных трансформерах.
This paper demonstrates the use of the first order logic in symbolic verification of the requirement specifications of reactive software
systems. We consider symbolic models of a specified system which are transition systems with symbolic states represented by formulae
of the first order logic. To efficiently compute predicate transformers the Satisfiability Modulo Theory methods are used instead of the
logical inference in the corresponding calculi.
Розглянуто використання логіки першого порядку у символьній верифікації специфікацій вимог програмного забезпечення, симво-
льні моделі систем, які є транзиційними системами з символьними станами представленими формулою логіки першого порядку. Ви-
користано методи Satisfiability Modulo Theory замість логічного виводу у відповідних численнях для ефективного обчислення у пре-
дикатних трансформерах.
Introduction. This paper demonstrates the use of
the first order logic in the verification of require-
ment specifications of reactive software systems.
The presented concepts have been implemented in
our VRS (Verification of Requirement Specificati-
ons) system [1–3]. The key algorithms used in VRS
for the verification of systems are presented. Speci-
fications of software systems in VRS are represen-
ted by means of systems of basic protocols. A basic
protocol is a formula of dynamic logic x ( (x, r)
< P(x, r) > (x, r)) and describes the local proper-
ties of a system in terms of pre- and postconditi-
ons and . Both are formulae of the first order
multisorted logic interpreted on a data domain, P is
a process, represented by means of an MSC dia-
gram [4, 5], and describes the evolution of the speci-
fied multi-agent system when triggered by the
precondition, x is a list of typed data variables, and
r is a list of environment and agent attributes.
Symbolic models of a specified system are tran-
sition systems with symbolic states represented by
formulae of the first order logic. To compute tran-
sitions of such models, basic protocols are interpre-
ted as predicate transformers: for a given symbolic
state of a system and a given basic protocol, the di-
rect predicate transformer [6] generates the next
symbolic state as its strongest postcondition and
the backward predicate transformer [6] generates
the previous symbolic state as its weakest precon-
dition. To efficiently compute the predicate trans-
formers we use SMT (Satisfiability Modulo The-
ory) methods instead of logical inference in the
corresponding calculi.
The deductive system of VRS supports the fol-
lowing data types: numeric (integer and real), sym-
bolic (free terms), enumerated, functions (arrays are
considered as functions with restricted domains),
and queues. This deductive system can be used for
static requirement verification of a system by pro-
ving that a set of basic protocols specifies a deter-
ministic system and is complete. Predicate trans-
formers can also be used for proving statically the
invariance of safety conditions, for dynamic veri-
fication of requirement specifications by generat-
ing traces of a symbolic system, and for finding
deadlocks or safety violations.
In the following section, the specification of a
system by means of basic protocols is formalized.
We define transition systems explaining the se-
mantics of such specifications for concrete and
symbolic models. In section “Base language”, we
give an overview of the logic used to express such
specifications in our VRS system. In the next sec-
tion we describe the one of main algorithms VRS
relies on during verification: the algorithm for
proving satisfiability of formulae, which integrate
symbolic and numeric information with behaviors
and functional data structures (which makes the
solvability of the SAT problem far from obvious).
Section “Verification” describes the use of these
algorithms for verification in the VRS system.
The conclusion briefly discusses related literature
and highlights opportunities for further work.
82 УСиМ, 2013, № 3
Basic Protocol Specifications
A basic protocols specification =< B, E) > of
a system consists of a set of basic protocols B to-
gether with an environment description E. E defi-
nes the signature of the language used to express
pre- and postconditions of the basic protocols and
the interpretation of this signature. We refer to the
language defined by the environment description
as the base language of a given specification; the
details of the base language are presented in the
next section. E also defines the set of attributes of
the specified system (symbols that may take dif-
ferent values over time). Each attribute is of sim-
ple or functional type. If an attribute f has functio-
nal type (1, 2, ) then attribute expressions
f (t1, t2, ) are available in basic protocols. Fur-
ther, the types, attributes, and behaviors of agents
inserted into an environment as well as the set of
possible initial states of agents and the environ-
ment are defined in the environment description.
The general form of a basic protocol is
( ( , ) ( , ) ( , ))x x r P x r x r . (1)
The variables x1, x2, in the list x = (x1, x2, )
are the parameter of a protocol and occur under
the quantifier together with their types: x = (x1 :
1, x2 : 2,). The list r used in the precondition
(x, r), the process P (x, r), and the postcondition
(x, r) of a basic protocol is the list of attribute
expressions. The precondition is a formula of the
base language, the process is an MSC diagram,
and the postcondition is a formula of the base lan-
guage extended by assignment statements (consi-
dered as temporal logic formula).
Each model of a specified system is a transi-
tion system with states represented in the form
s[m1 : u1, m2 : u2,] where s is the kernel of the
environment state, m1, m2, are the names of agents,
and u1, u2, are the behaviors of these agents
considered as their states.
All models are the instances of a model of the
interaction of agents and environments [7, 8], and
a basic protocol specification can be interpreted as
a method for defining the insertion function.
The actions of a model are instantiated basic
protocols considered atomic (i.e., we do not con-
sider the individual steps in the process of the ba-
sic protocol). Depending on how we represent the
kernel of the environment state we can distinguish
various kinds of models: Concrete models repre-
sent the state as mappings from the set of attribute
expressions to their concrete values. Symbolic mo-
dels represent the state as formulae of the base lan-
guage. Symbolic models are further differentiated
based on the condition under which we consider a
basic protocol applicable to a symbolic state (r).
For universal models, the applicability condition
is the validity of implication (r) x (x, r). For
existential models, a basic protocol is applicable if
(r) x (x, r) is satisfiable. In this paper we con-
sider existential symbolic models and their rela-
tionship to concrete models.
Concrete models. A concrete model C defined
by the environment description is constructed as
follows. A constant attribute expression is an at-
tribute of a simple type or an attribute expression
of the form f (a1, a2, ), where f is an attribute of a
functional type and a1, a2, are constant (ground)
expressions of corresponding types. Let A be the
set of all constant attribute expressions. The ker-
nel of the state of a concrete model is a partial
mapping s : A D from the set of constant at-
tribute expressions to the data domain D (its val-
ues). This mapping must preserve the types: if
s (x) is defined then the type of s (x) is equal to the
type of x. The complete the state of environment
s[m1 : u1, m2 : u2,] contains all agents inserted
into the environment.
The mapping s is extended in a natural way to
terms and formulae of a base language through
iterative substitution of the values for attribute ex-
pressions, and we say that a formula is valid on
the state s of a concrete model (denoted |s ) if
s() is defined and valid.
Let ( ( , ) ( , ) ( , ))B x x y P x y x y be a
basic protocol, x = x1, x2, the parameters of B
and a = a1, a2, a list of values such that the
type of ai is contained in the type of parameter xi
(types are partially ordered). A formula B (a) =
( ( , ) ( , ) ( , ))x a y P a y a y is called an
instantiation of a protocol B . Let [ : ]s m u
1 1 2 2[ : , : , ]s m u m u and ],:,:[ 2211 umums be
УСиМ, 2013, № 3 83
the states of a concrete model. Define the transi-
tion relation of a system C in such a way that
( )[ : ] [ : ] ( [ : ]| ( : )B as m u s m u s m u m u
( , )) ( [ : ] |a r s m u ( : ) ( , )])m u a r where
1 1 2 2 1 1( : ) ( : ) ( : ) ,( : ) ( : )m u m u m u m u m u
2 2( : )m u An expression ):( ii um asserts that
an agent mi is in a state ui and is referred to as a
state assertion.
A transition function defined in this manner
may exhibit a high degree of non-determinism.
For example, attributes that do not occur in a post-
condition may possess arbitrary values and agents
that do not occur in the state assumption of a post-
condition can change their states arbitrarily. Such
nondeterminism can be restricted in a usual way,
by restricting that only attribute expressions oc-
curring in postconditions of instantiated basic pro-
tocols can change their values and that only agents
occurring in such postconditions can change their
states (independency constraint). This is possible
as in concrete models the values of attribute ex-
pressions and the states of agents are independent.
Symbolic models. The kernel of the environment
state for an existential symbolic model is a for-
mula of the base language. An environment state has
the form (r) [m : u] = (r) [m1 : u1, m2 : u2,] where
(r) is a formula, and [m : u] defines the states of
all agents inserted into the environment. The tran-
sition relation must satisfy the following minimal
constraints, given ( )[ : ] Br m u ( )[ : ]r m u :
( ) ( : ) ( , )r m u x x r must be satisfiable
(applicability condition).
( ) ( : ) ( , )r m u x x r (postcondition re-
quirement).
Let ]:[]:[ umsums B be an arbitrary
transition of a concrete model C ; if [ : ] |s m u
| ( ) ( : )r m u and ( )[ : ] | ( )[ : ]Br m u r m u
then [ : ] | ( ) ( : )s m u r m u (simulation requi-
rement).
Under these minimal restrictions, the system
again may be highly non-deterministic. More de-
terministic means of defining the transition rela-
tion will be considered below in terms of predi-
cate transformers.
Base language
The underlying language (base language) to cap-
ture specifications is a first order multisorted langu-
age with interpreted and uninterpreted functional
symbols. The interpreted functional symbols charac-
terize the environment and are used for the definiti-
on of transition functions, as discussed in the previ-
ous section. Uninterpreted symbols are used to rep-
resent the changing state of the environment and are
identified with attributes of a system. All uninterpre-
ted symbols have types, and thus their possible inter-
pretations are restricted by definite domains and
ranges of values. Functional symbols of arity 0 cor-
respond to simple attributes, others correspond to the
attributes of functional types or functional attributes.
We rely on the following types (sorts) of func-
tional symbols: integer, real, boolean, symbolic, and
a set of enumerated data types are defined as sim-
ple types. For all types the equality predicate is
defined. For numeric types the inequality relation is
defined, but and only addition and multiplication
by constants of the corresponding type are allowed
as operations (interpreted functions). Consequential-
ly, arithmetic is limited to linear arithmetic. The do-
main for a symbolic type is a set of free terms con-
structed from symbolic and numeric constants by
means of a set of predefined constructors. Enumer-
ated data types provide sets of possible values. For
list types, access functions are defined, and lists can
change their values by adding or removing elements
to (from) head or tail only. Thus, list types exhibit the
behavior of queues. Behavior types are used as agent
states and are considered as elements of behavior
algebra [8] (a kind of process algebra). This algebra
has two operations: prefixing ua. (a is an action, u
is a behavior), and nondeterministic choice u + v. It
has also three constants: dead lock 0, successful ter-
mination and undefined behavior . The behavi-
or algebra is generated by constants, actions (arbi-
trary symbolic constant expressions can be used as
actions) and predefined constant behaviors. The last
are defined in environment description as minimal
solutions of a system of equations in behavior alge-
bra. Functional types are functions from simple types
to simple types with arbitrary arity. Arrays are at-
tributes of functional types with arguments (in-
dexes) limited to enumerated types or integers.
84 УСиМ, 2013, № 3
All simple types may occur in symbolic data
structures. Formulae describing precondition, post-
condition and the kernel state of the environment
for symbolic models may use only existential qu-
antifiers in positive positions (when there is an
even number of negations on any branch leading
to the quantifier). Quantifiers can bind only vari-
ables of simple types. In preconditions, list data
can be used only in access functions. The general
form of a precondition is (x, r) F (x, r), where
(x, r) = (m1 : u1) (m2 : u2) is a conjunction
of state assumptions and F (x, r) does not contain
state assumptions. A postcondition is a conjunc-
tion of arbitrary formulae of the base language,
state assumptions, and assignments. A simple as-
signment has the form x := y, where x is an attrib-
ute expression and y is an expression of a type that
is contained in the type of x and asserts that the
new value of x is the old value of the expression y.
A list assignment adds or removes from the head
or tail of a list. The general form of the postcondi-
tion is (x, r) R (x, r) L (x, r) F (x, r) where (x, r)
is a conjunction of state assumptions, R (x, r) is a
conjunction of simple assignments, L(x, r) is a con-
junction of list updating, and F (x, r) is a formula
of the base language without state assumptions.
Assignments are tied to two states: before the ap-
plication of a basic protocol and after its application,
and thus can be considered as temporal logic formu-
lae. Simple assignments can be easily eliminated
from basic protocols. For example, the basic proto-
col x (x, r) P(x, r) (u (v) := w)) F is equi-
valent to the basic protocol x (y, z) (x, r)
(y = v) (z = w) P(x, r) (u (y) := z)) F. List
updating can also be eliminated by a small exten-
sion of the base language. Thus, in the previous
section we did not consider assignments as part of
specification models.
The general form of the kernel state of the en-
vironment is x (L(x) F (x)), where F (x) is a
formula of the base language without list type ex-
pressions and L(x) is a conjunction of equalities of
the form x = y, where x is a constant attribute ex-
pression of a list type and y is a list expression.
Satisfiability
The main functionality of the deductive system
of VRS is to check the satisfiability of formulae of
the base language. This is used in determining the
applicability of basic protocols and in computing
predicate transformers.
The applicability of the basic protocol (1) in envi-
ronment state (r)[m : u] = (r) [m1 : u1, m2 : u2,]
is equivalent to the satisfiability of the formula
( ) ( : ) ( , )r m u x x r . (2)
Checking satisfiability of this formula proceeds
in four steps: elimination of state assumptions, elimi-
nation of list access functions, elimination of functi-
onal attributes, proving closed formula without attri-
bute expressions. These steps are discussed below.
Elimination of state assumptions. Satisfiability
of a state assumption given a precondition and a
state of the environment is checked by means of
matching concrete state assumptions of the environ-
ment state and state assumptions depending on pa-
rameters and attribute expressions, both considered
as matching variables. Matching is performed mo-
dulo the following relations: m : (u + v) = (m : u)
(m : v), (m : a.u = n : b.v) (m = n) (a = b)
(u = v). The result will be a new constraint (x, y)
that replaces state assumptions (x, y) in precondi-
tion and environment state, after which the for-
mula does not depend on state assumptions. Note
that there can be multiple results depending on
which the state assumptions were matched, where
each result gives explicit values for parameters
and attribute expressions occurring in the precon-
dition. To prove satisfiability we need only one
solution, so these are considered one by one.
Elimination of list access functions. We com-
pute the instantiations of the empty list predicate
and the accessor functions. In both cases, a list is
matched against u (x, r). The value of the empty list
predicate is set to 0 or 1, depending on whether the
match succeeded. For accessors, we either obtain a
simple type expression a returned from an acces-
sor, or a a new variable v of type (the type of the
list expression) is generated and added to quanti-
fier prefix (initially empty) of the formula (2). The
accessor is set equal to either a or v. The matching
of attribute expressions can have several results.
Different results are represented as a disjunction
of formulae.
First, superpositions of functional expressions are
eliminated by the successive substitution of every
УСиМ, 2013, № 3 85
innermost occurrence of f (x) by a new variable, y
bound with an existential quantifier, and adding 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 of such replacements, there will be no more nes-
ted functional expressions. For every attribute ex-
pression f of array or functional type, all its occur-
rences f (x1), f (x2), with different parameters x1,
x2, are considered: f (xi) is replaced by variable yi,
bound with an existential quantifier, and equations
(xi = xj) (yi = yj) are added. At this point, there will
be only simple attributes and the method for sim-
ple attributes is applied. Elimination of functional
expressions imposes restrictions on the range of
values of arguments for the functional attributes of
type array with integer or enumerated indexes. For
example, if the attribute f has a type array(m, ),
where m is a number, and is an enumerated type
with constants a1, a2,, then during elimination of
functional expression f (i, u), the generated formula
will include conjunctive constraints 0 i i m – 1
(u = a1 u = a2 .
The result is a closed formula (i.e. a formula
not containing attributes) and all bound variables
have types integer, real, or symbolic, or are enu-
merated types.
Proving a closed formula without attribute
expressions. The deductive system of VRS con-
tains three specialized provers: an integer prover
for Pressburger arithmetic, the Furie–Motskin al-
gorithm for linear arithmetic over reals, and a sym-
bolic prover that includes an algorithm of finding
the most general solution for a system of symbolic
equations (modified Montanari–Rossi algorithm
of unification integrated with numerical provers).
The method of proving closed formulae first re-
duces a formula to prenex normal form and tries
to prove it by simple reductions and simplificati-
ons. If this is not successful, then the specialized
provers are invoked. The first step of the reduction
eliminates symbolic constructors. All symbolic equ-
alities of the form t1 = t2 in which t1 and t2 are not
variables are analyzed. If, for example, t1 = f1(a1, a2),
t2 = f 2 (b1, b2), where f1, f2 are symbolic constructors
such that f1 = f2, then this equality is replaced by the
equivalent conjunction of equalities a1 = b1 a2 = b2.
For different constructors, t1 = t2 is replaced with 0.
After that all possible substitutions of variables
are performed. Given a literal v = e, occurrences
of variable v are replaced with e, if e does not de-
pend on v and if the type of v includes the type of
e. If a symbolic variable v occurs in expression e,
the equality is impossible and is replaced by 0.
Similarly, 0 is substituted for type mismatches.
Then enumerated types are eliminated. The na-
ive method of replacing a subformula of a form
x P(x) where x is a variable of enumerated type
with values a1, a2, by the disjunction P(a1)
P(a2) is too inefficient due to the large ex-
pressions created. Instead, we rely on recursive eli-
mination: after maximally narrowing the scopes of
quantifiers, the formulae are proved inside out, ex-
panding the above existential quantification only
when a recursive proof was successful.
To prove a closed formula without enumerated
types it is reduced to a disjunction of conjunctions
of literals bounded with existential quantifiers. It
is now sufficient to prove one of these conjunc-
tions. They are transformed to prenex normal form,
and a proof search begins. All literals are divided
into three groups: equalities, negation of equalities
and numerical inequalities. At first, the system of
symbolic–numerical equalities is solved. If this sys-
tem is consistent, then the most general solution
v1 = e1 v1 = e2 , where expressions e1, e2, do
not depend upon variables v1, v2, is found. Variab-
les v1, v2, are eliminated by a substitution of e1,
e2, instead of the corresponding variables in a for-
mula. Now there are only negations of equalities
and numerical inequalities. Symbolic negations of
equalities p q are eliminated by finding the most
general solution of equality p = q. If this solution
does not exist, then the negation is true and can be
deleted. If a general solution v = t for some symbolic
variable v exists, the symbolic variables can take on
infinitely many values, and therefore it is possible
for this variable to take on a value which make equ-
ality v = t false. Therefore a literal p q is solvable
and can be removed. If a general solution contains
numerical equalities only, we add the negation of
this solution to the numerical inequalities. After the
removal of all solved negations with symbolic vari-
ables, there remains a pure numerical formula
which is solved by the appropriate numerical prover.
86 УСиМ, 2013, № 3
Verification
The input language of VRS expresses require-
ments specifications for systems through basic pro-
tocols. The details of this language have been deter-
mined based on a large number of industrial pro-
jects aimed at the development of software for distri-
buted reactive systems in various industries. These
notations include only some abstractions neces-
sary for the eventual description of algorithms and
ignores details connected with the representation
of the process part. Neither is efficiency a concern
at this point. VRS allows the use of various repre-
sentations of requirements, from tabular forms to
scenario languages. These representations are trans-
lated into basic protocols by front-end tools.
VRS is comprised of two groups of tools. The
first group is aimed at static requirement checking
(SRC), the second is aimed at the dynamic verifi-
cation of system behavior.
SRC is supported by the following tools: a con-
sistency checker, a completeness checker, a safety
checker, and a reachability checker. A basic pro-
tocol specification is consistent if under the same
state assumptions there is only one basic protocol
that can be applied. This condition ensures deter-
minism of a specified system comprised of behav-
iors of agents that may be nondeterminate. Con-
sistency is checked by proving the satisfiability of
the preconditions of arbitrary two protocols. If
their conjunction is not satisfiable they are consis-
tent. Completeness is considered to be the validity
of the disjunction of preconditions of basic proto-
cols with the same state assumptions and is checked
by means of a satisfiability algorithm, i.e., its ne-
gation must be unsatisfiable. Completeness is a
sufficient condition for the absence of dead locks.
Both consistency and completeness conditions
are only sufficient. If a violation has been found
we must prove that such state is reachable from
the initial states of a system. For this purpose the
static reachability checker can be used which tries
to prove the safety of the negation of such viola-
tion. The reachability checker and the safety checker
use the direct predicate transformer defined above.
To prove that a given condition is a safety condi-
tion, the checker generates the following invari-
ants: if a condition is valid before applying a basic
protocol, then it will be valid after its application.
Dynamic verification tools generate traces of a
model of the specified system. We provide two trace
generators: The concrete trace generator (CTG)
works with concrete models of a system and uses
a restricted base language limiting assignment sta-
tements to the postconditions. The CTG is similar to
a model checker and uses heuristics and abstractions
to reduce the state space, decrease interleaving, etc.
The symbolic trace generator (STG) imposes no re-
strictions on the base language and uses both direct
and backward predicate transformers[6]. The former
is used for search for traces from initial to goal sta-
tes, the latter is used for finding traces from a goal
state to initial states. STG and CTG rely on a com-
mon generating engine and common tools for con-
troling the search. Both generators can be controled
by intermediate goal states and check the validity
of given or predefined safety conditions, such as the
absence of dead locks in the traversed state space.
Conclusions
We have outlined the key algorithms used in the VRS sys-
tem for the symbolic verification of requirement specifications.
VRS was successfully piloted in a number of industrial pro-
jects in a large corporation. The main application domains were
telecommunication, automotive, and telematics. Industrial pro-
jects successively piloted using VRS consisted of up to 10,000
requirements formalized as basic protocols, with over thousand
attributes. Substantial numbers of requirements defects were
detected by applying the VRS tools to these industrial spe-
cifications. The trace generators have also been leveraged for
the generation of tests, and verified specifications have been
used as the starting point for further product development.
The theoretical foundation of VRS is the theory of inter-
action of agents and environments [7, 8], now referred to as in-
sertion modeling [9]. Traditional mathematical models for spe-
cifications of concurrent systems usually are based on process
algebras (CSP [10], CCS [11], Lotos, ACP, CRL, -calculus,
etc.), temporal and dynamic logics (LPTL, LTL, CTL, CTL*,
PDL), and automata models.
Temporal logic is a formal specification language for the
description of behavioral properties of non-terminating and
interacting (reactive) systems. Traditional one distinguishes
between safety (“something bad never happens”), liveness
(“something good will eventually happen”), and various fair-
ness properties. For example, Lamport's TLA (Temporal Logic
of Actions) [12, 13] is aimed at the description of such prop-
erties and is based on Pnueli's temporal logic [14] with as-
signment, enriched signatures, and module specifications.
Many temporal logics are decidable and corresponding
decision procedures exist for linear and branching time logics
[15], propositional modal logic [16], and some variants of
CTL* [17]. In such decision procedures techniques from auto-
mata theory, semantic tableaux, or binary decision diagrams
(BDD) [18] have been used. Typically, a system to be verified
УСиМ, 2013, № 3 87
is modeled as a (finite) state transition graph, and the pro-
perties are formulated in an appropriate temporal logic. An
efficient search procedure is then used to determine whether
the state transition graph satisfies the temporal formula or
not. This technique was first developed by Clarke and Emer-
son [19], and by Quielle and Sifakis [20] and extended later
by Burch et.al. [21].
In the current version of our VRS system, temporal for-
mulae are represented implicitly and are evaluated by check-
ing algorithms. Enhancements are planned to allow the ex-
plicit representation of temporal formulae.
The most closely related verification tools to our approach
are the SCR toolset [22] and the Action Language Verifier
[23]. Different from these systems, VRS uses MSC [4, 5] as
the language for capturing the process part of system re-
quirements. This choice of representation was guided by our
experience in applying our tools in industrial projects. Pow-
erful extensions to MSC have been proposed: Live Sequence
Charts (LSC [24]), Triggered Message Sequence Charts
(TMSC [25]), and Object Message Sequence Charts (OMSC
[26]). We are investigating similar extensions to the repre-
sentation of basic protocols as well as new algorithms for
symbolic checking and invariant construction.
1. Basic Protocols, Message Sequence Charts, and the Ve-
rification of Requirements Specifications / A.Ad. Leti-
chevsky, Ju.V. Kapitonova, A.A. Letichevsky et al.
// Computer Networks. – 2005. – 47. – P. 662–675.
2. Validation of Embedded Systems / Ju. Kapitonova, A. Le-
tichevsky, V. Volkov et al. R. Zurawski (Ed.) // The Em-
bedded Systems Handbook. – Miami: CRC Press, 2005.
3. System Specification with Basic Protocols / Ju. Kapi-
tonova, A. Letichevsky, V. Volkov et al. // Cybernetics
and System Analyses. – 2005. – 4. – P. 3–21.
4. International Telecommunications Union. ITU-T Rec-
ommendation Z.120: Message Sequence Charts. Ge-
neva, ITU-T, 2002.
5. International Telecommunications Union. Recommenda-
tion Z.120 Annex B: Formal semantics of Message
Sequence Charts, 1998.
6. Properties of Predicate Transformer of VRS System /
A.Ad. Letichevsky, A.B. Godlevsky, A.A. Letichevsky et
al. // Cybernetics and System Analyses. – 2010. – 4. –
P. 3–16.
7. Letichevsky A., Gilbert D. A Model for Interaction of
Agents and Environments / D. Bert, C. Choppy, P. Moses
(Eds.) // Recent Trends in Algebraic Development Tech-
niques. Lecture Notes in Comp. Sci. 1827, Springer, 1999.
8. Letichevsky A. Algebra of behavior transformations and
its applications / V.B. Kudryavtsev, I.G. Rosenberg
(Eds.) // Structural theory of Automata, Semigroups, and
Universal Algebra, NATO Science Series II. Mathema-
tics, Physics and Chemistry. – Springer 2005. – 207. –
P. 241–272.
9. Insertion modeling in distributed system design / A. Le-
tichevsky, Ju. Kapitonova, V. Kotlyarov et al. // Prob-
lems in Programming. – 2008. – 4. – P. 13–39.
10. Hoare C.A.R. Communicating Sequential Processes.
Prentice Hall, 1985.
11. Milner R. Communication and Concurrency. Prentice
Hall, 1989.
12. Lamport L. Introduction to TLA. SRC Technical Note
1994-001, 1994.
13. Lamport L. The temporal logic of actions // ACM Trans-
actions on Programming Languages and Systems, May
1994. – P. 872–923.
14. Pnueli A. The temporal logic of programs // Proc. of the
18th Annual Symposium on the Foundations of Comp.
Sci., Nov. 1977. – P. 46–52.
15. Emerson E., Halpern J. Decision procedures and ex-
pressiveness in the temporal logic of branching time //
J. of Comp. and System Sci. – 1985. – 30 (1). – P. 1–24.
16. Fisher M. Ladner R. Propositional modal logic of pro-
grams // Proc. 9th ACM Ann. Symp. on Theory of
Computing, Boulder, Col., May 1977. – P. 286–294.
17. Emerson E. Temporal and modal logic / J. van Leeu-
wen (Ed.) // Handbook of Theoretical Comp. Sci. – El-
sevier, (B). – 1990. – P. 997–1072.
18. Bryant R. Graph-based algorithms for Boolean func-
tion manipulation // IEEE Transactions on Computers. –
1986. – 35 (8). – P. 677–691,
19. Clarke E. Emerson E. Synthesis of synchronization ske-
letons for branching time temporal logic // The Work-
shop on Logic of Programs, Lecture Notes in Computer
Science, Springer Verlag, 1981. – 131. – P. 128–143.
20. Quielle J. Sifakis J. Specification and verification of
concurrent systems in CESAR // Proc. 5th Intern.
Symp. on Programming, 1981. – P. 142–158.
21. Symbolic model checking: 1020 states and beyond /
J. Burch, E. Clarke, K. McMillan et al. // Information
and Computation, 1002. – 98 (2). – P. 142–170.
22. Tools for constructing requirements specifications: The
SCR toolset at the age of ten / C. Heitmeyer, M. Archer,
R. Bharadwaj et al. // Computer Systems Science &
Engineering,2005. – 1. – P. 19–35.
23. Bultan T., Yavuz-Kahveci T. Action language verifier //
Proc. of ASE 2001, November 2001. – P. 382–386.
24. Harel D., Marelly R. Come, Let's Play: Scenario-Based
programming Using LSCs and the Play-Engine. Sprin-
ger 2003.
25. Sengupta B., Cleaveland R. Triggered Message Sequ-
ence Charts // Proceedings of SIGSOFT 2002/FSE–10,
ACM Press, 2002. – P. 167–176.
26. Pattern-Oriented Software Architecture-A System of
Patterns / F. Buschmann, R. Meunier, H. Rohnert et al. //
Wiley & Sons. – New York, 1996.
Поступила 22.06.2012
Тел. для справок: +38 095 324-1557, +38 055 246-7070
(Киев, Миссури, Херсон)
E-mail: vladim@ksu.ks.ua, vladimirius@gmail.com
© A.Ад. Летичевский, A.А. Летичевский, T. Вейгерт,
В.С. Песчаненко, 2013
<<
/ASCII85EncodePages false
/AllowTransparency false
/AutoPositionEPSFiles true
/AutoRotatePages /None
/Binding /Left
/CalGrayProfile (Dot Gain 20%)
/CalRGBProfile (sRGB IEC61966-2.1)
/CalCMYKProfile (U.S. Web Coated \050SWOP\051 v2)
/sRGBProfile (sRGB IEC61966-2.1)
/CannotEmbedFontPolicy /Error
/CompatibilityLevel 1.4
/CompressObjects /Tags
/CompressPages true
/ConvertImagesToIndexed true
/PassThroughJPEGImages true
/CreateJobTicket false
/DefaultRenderingIntent /Default
/DetectBlends true
/DetectCurves 0.0000
/ColorConversionStrategy /CMYK
/DoThumbnails false
/EmbedAllFonts true
/EmbedOpenType false
/ParseICCProfilesInComments true
/EmbedJobOptions true
/DSCReportingLevel 0
/EmitDSCWarnings false
/EndPage -1
/ImageMemory 1048576
/LockDistillerParams false
/MaxSubsetPct 100
/Optimize true
/OPM 1
/ParseDSCComments true
/ParseDSCCommentsForDocInfo true
/PreserveCopyPage true
/PreserveDICMYKValues true
/PreserveEPSInfo true
/PreserveFlatness true
/PreserveHalftoneInfo false
/PreserveOPIComments true
/PreserveOverprintSettings true
/StartPage 1
/SubsetFonts true
/TransferFunctionInfo /Apply
/UCRandBGInfo /Preserve
/UsePrologue false
/ColorSettingsFile ()
/AlwaysEmbed [ true
]
/NeverEmbed [ true
]
/AntiAliasColorImages false
/CropColorImages true
/ColorImageMinResolution 300
/ColorImageMinResolutionPolicy /OK
/DownsampleColorImages true
/ColorImageDownsampleType /Bicubic
/ColorImageResolution 300
/ColorImageDepth -1
/ColorImageMinDownsampleDepth 1
/ColorImageDownsampleThreshold 1.50000
/EncodeColorImages true
/ColorImageFilter /DCTEncode
/AutoFilterColorImages true
/ColorImageAutoFilterStrategy /JPEG
/ColorACSImageDict <<
/QFactor 0.15
/HSamples [1 1 1 1] /VSamples [1 1 1 1]
>>
/ColorImageDict <<
/QFactor 0.15
/HSamples [1 1 1 1] /VSamples [1 1 1 1]
>>
/JPEG2000ColorACSImageDict <<
/TileWidth 256
/TileHeight 256
/Quality 30
>>
/JPEG2000ColorImageDict <<
/TileWidth 256
/TileHeight 256
/Quality 30
>>
/AntiAliasGrayImages false
/CropGrayImages true
/GrayImageMinResolution 300
/GrayImageMinResolutionPolicy /OK
/DownsampleGrayImages true
/GrayImageDownsampleType /Bicubic
/GrayImageResolution 300
/GrayImageDepth -1
/GrayImageMinDownsampleDepth 2
/GrayImageDownsampleThreshold 1.50000
/EncodeGrayImages true
/GrayImageFilter /DCTEncode
/AutoFilterGrayImages true
/GrayImageAutoFilterStrategy /JPEG
/GrayACSImageDict <<
/QFactor 0.15
/HSamples [1 1 1 1] /VSamples [1 1 1 1]
>>
/GrayImageDict <<
/QFactor 0.15
/HSamples [1 1 1 1] /VSamples [1 1 1 1]
>>
/JPEG2000GrayACSImageDict <<
/TileWidth 256
/TileHeight 256
/Quality 30
>>
/JPEG2000GrayImageDict <<
/TileWidth 256
/TileHeight 256
/Quality 30
>>
/AntiAliasMonoImages false
/CropMonoImages true
/MonoImageMinResolution 1200
/MonoImageMinResolutionPolicy /OK
/DownsampleMonoImages true
/MonoImageDownsampleType /Bicubic
/MonoImageResolution 1200
/MonoImageDepth -1
/MonoImageDownsampleThreshold 1.50000
/EncodeMonoImages true
/MonoImageFilter /CCITTFaxEncode
/MonoImageDict <<
/K -1
>>
/AllowPSXObjects false
/CheckCompliance [
/None
]
/PDFX1aCheck false
/PDFX3Check false
/PDFXCompliantPDFOnly false
/PDFXNoTrimBoxError true
/PDFXTrimBoxToMediaBoxOffset [
0.00000
0.00000
0.00000
0.00000
]
/PDFXSetBleedBoxToMediaBox true
/PDFXBleedBoxToTrimBoxOffset [
0.00000
0.00000
0.00000
0.00000
]
/PDFXOutputIntentProfile ()
/PDFXOutputConditionIdentifier ()
/PDFXOutputCondition ()
/PDFXRegistryName ()
/PDFXTrapped /False
/CreateJDFFile false
/Description <<
/ARA <FEFF06270633062A062E062F0645002006470630064700200627064406250639062F0627062F0627062A002006440625064606340627062100200648062B062706260642002000410064006F00620065002000500044004600200645062A064806270641064206290020064406440637062806270639062900200641064A00200627064406450637062706280639002006300627062A0020062F0631062C0627062A002006270644062C0648062F0629002006270644063906270644064A0629061B0020064A06450643064600200641062A062D00200648062B0627062606420020005000440046002006270644064506460634062306290020062806270633062A062E062F062706450020004100630072006F0062006100740020064800410064006F006200650020005200650061006400650072002006250635062F0627063100200035002E0030002006480627064406250635062F062706310627062A0020062706440623062D062F062B002E0635062F0627063100200035002E0030002006480627064406250635062F062706310627062A0020062706440623062D062F062B002E>
/BGR <FEFF04180437043f043e043b043704320430043904420435002004420435043704380020043d0430044104420440043e0439043a0438002c00200437043000200434043000200441044a0437043404300432043004420435002000410064006f00620065002000500044004600200434043e043a0443043c0435043d04420438002c0020043c0430043a04410438043c0430043b043d043e0020043f044004380433043e04340435043d04380020043704300020043204380441043e043a043e043a0430044704350441044204320435043d0020043f04350447043004420020043704300020043f044004350434043f0435044704300442043d04300020043f043e04340433043e0442043e0432043a0430002e002000200421044a04370434043004340435043d043804420435002000500044004600200434043e043a0443043c0435043d044204380020043c043e0433043004420020043404300020044104350020043e0442043204300440044f0442002004410020004100630072006f00620061007400200438002000410064006f00620065002000520065006100640065007200200035002e00300020043800200441043b0435043404320430044904380020043204350440044104380438002e>
/CHS <FEFF4f7f75288fd94e9b8bbe5b9a521b5efa7684002000410064006f006200650020005000440046002065876863900275284e8e9ad88d2891cf76845370524d53705237300260a853ef4ee54f7f75280020004100630072006f0062006100740020548c002000410064006f00620065002000520065006100640065007200200035002e003000204ee553ca66f49ad87248672c676562535f00521b5efa768400200050004400460020658768633002>
/CHT <FEFF4f7f752890194e9b8a2d7f6e5efa7acb7684002000410064006f006200650020005000440046002065874ef69069752865bc9ad854c18cea76845370524d5370523786557406300260a853ef4ee54f7f75280020004100630072006f0062006100740020548c002000410064006f00620065002000520065006100640065007200200035002e003000204ee553ca66f49ad87248672c4f86958b555f5df25efa7acb76840020005000440046002065874ef63002>
/CZE <FEFF005400610074006f0020006e006100730074006100760065006e00ed00200070006f0075017e0069006a007400650020006b0020007600790074007600e101590065006e00ed00200064006f006b0075006d0065006e0074016f002000410064006f006200650020005000440046002c0020006b00740065007200e90020007300650020006e0065006a006c00e90070006500200068006f006400ed002000700072006f0020006b00760061006c00690074006e00ed0020007400690073006b00200061002000700072006500700072006500730073002e002000200056007900740076006f01590065006e00e900200064006f006b0075006d0065006e007400790020005000440046002000620075006400650020006d006f017e006e00e90020006f007400650076015900ed007400200076002000700072006f006700720061006d0065006300680020004100630072006f00620061007400200061002000410064006f00620065002000520065006100640065007200200035002e0030002000610020006e006f0076011b006a016100ed00630068002e>
/DAN <FEFF004200720075006700200069006e0064007300740069006c006c0069006e006700650072006e0065002000740069006c0020006100740020006f007000720065007400740065002000410064006f006200650020005000440046002d0064006f006b0075006d0065006e007400650072002c0020006400650072002000620065006400730074002000650067006e006500720020007300690067002000740069006c002000700072006500700072006500730073002d007500640073006b007200690076006e0069006e00670020006100660020006800f8006a0020006b00760061006c0069007400650074002e0020004400650020006f007000720065007400740065006400650020005000440046002d0064006f006b0075006d0065006e0074006500720020006b0061006e002000e50062006e00650073002000690020004100630072006f00620061007400200065006c006c006500720020004100630072006f006200610074002000520065006100640065007200200035002e00300020006f00670020006e0079006500720065002e>
/DEU <FEFF00560065007200770065006e00640065006e0020005300690065002000640069006500730065002000450069006e007300740065006c006c0075006e00670065006e0020007a0075006d002000450072007300740065006c006c0065006e00200076006f006e002000410064006f006200650020005000440046002d0044006f006b0075006d0065006e00740065006e002c00200076006f006e002000640065006e0065006e002000530069006500200068006f006300680077006500720074006900670065002000500072006500700072006500730073002d0044007200750063006b0065002000650072007a0065007500670065006e0020006d00f60063006800740065006e002e002000450072007300740065006c006c007400650020005000440046002d0044006f006b0075006d0065006e007400650020006b00f6006e006e0065006e0020006d006900740020004100630072006f00620061007400200075006e0064002000410064006f00620065002000520065006100640065007200200035002e00300020006f0064006500720020006800f600680065007200200067006500f600660066006e00650074002000770065007200640065006e002e>
/ESP <FEFF005500740069006c0069006300650020006500730074006100200063006f006e0066006900670075007200610063006900f3006e0020007000610072006100200063007200650061007200200064006f00630075006d0065006e0074006f00730020005000440046002000640065002000410064006f0062006500200061006400650063007500610064006f00730020007000610072006100200069006d0070007200650073006900f3006e0020007000720065002d0065006400690074006f007200690061006c00200064006500200061006c00740061002000630061006c0069006400610064002e002000530065002000700075006500640065006e00200061006200720069007200200064006f00630075006d0065006e0074006f00730020005000440046002000630072006500610064006f007300200063006f006e0020004100630072006f006200610074002c002000410064006f00620065002000520065006100640065007200200035002e003000200079002000760065007200730069006f006e0065007300200070006f00730074006500720069006f007200650073002e>
/ETI <FEFF004b00610073007500740061006700650020006e0065006900640020007300e4007400740065006900640020006b00760061006c006900740065006500740073006500200074007200fc006b006900650065006c007300650020007000720069006e00740069006d0069007300650020006a0061006f006b007300200073006f00620069006c0069006b0065002000410064006f006200650020005000440046002d0064006f006b0075006d0065006e00740069006400650020006c006f006f006d006900730065006b0073002e00200020004c006f006f0064007500640020005000440046002d0064006f006b0075006d0065006e00740065002000730061006100740065002000610076006100640061002000700072006f006700720061006d006d006900640065006700610020004100630072006f0062006100740020006e0069006e0067002000410064006f00620065002000520065006100640065007200200035002e00300020006a00610020007500750065006d006100740065002000760065007200730069006f006f006e00690064006500670061002e000d000a>
/FRA <FEFF005500740069006c006900730065007a00200063006500730020006f007000740069006f006e00730020006100660069006e00200064006500200063007200e900650072002000640065007300200064006f00630075006d0065006e00740073002000410064006f00620065002000500044004600200070006f0075007200200075006e00650020007100750061006c0069007400e90020006400270069006d007000720065007300730069006f006e00200070007200e9007000720065007300730065002e0020004c0065007300200064006f00630075006d0065006e00740073002000500044004600200063007200e900e90073002000700065007500760065006e0074002000ea0074007200650020006f007500760065007200740073002000640061006e00730020004100630072006f006200610074002c002000610069006e00730069002000710075002700410064006f00620065002000520065006100640065007200200035002e0030002000650074002000760065007200730069006f006e007300200075006c007400e90072006900650075007200650073002e>
/GRE <FEFF03a703c103b703c303b903bc03bf03c003bf03b903ae03c303c403b5002003b103c503c403ad03c2002003c403b903c2002003c103c503b803bc03af03c303b503b903c2002003b303b903b1002003bd03b1002003b403b703bc03b903bf03c503c103b303ae03c303b503c403b5002003ad03b303b303c103b103c603b1002000410064006f006200650020005000440046002003c003bf03c5002003b503af03bd03b103b9002003ba03b103c42019002003b503be03bf03c703ae03bd002003ba03b103c403ac03bb03bb03b703bb03b1002003b303b903b1002003c003c103bf002d03b503ba03c403c503c003c903c403b903ba03ad03c2002003b503c103b303b103c303af03b503c2002003c503c803b703bb03ae03c2002003c003bf03b903cc03c403b703c403b103c2002e0020002003a403b10020005000440046002003ad03b303b303c103b103c603b1002003c003bf03c5002003ad03c703b503c403b5002003b403b703bc03b903bf03c503c103b303ae03c303b503b9002003bc03c003bf03c103bf03cd03bd002003bd03b1002003b103bd03bf03b903c703c403bf03cd03bd002003bc03b5002003c403bf0020004100630072006f006200610074002c002003c403bf002000410064006f00620065002000520065006100640065007200200035002e0030002003ba03b103b9002003bc03b503c403b103b303b503bd03ad03c303c403b503c103b503c2002003b503ba03b403cc03c303b503b903c2002e>
/HEB <FEFF05D405E905EA05DE05E905D5002005D105D405D205D305E805D505EA002005D005DC05D4002005DB05D305D9002005DC05D905E605D505E8002005DE05E105DE05DB05D9002000410064006F006200650020005000440046002005D405DE05D505EA05D005DE05D905DD002005DC05D405D305E405E105EA002005E705D305DD002D05D305E405D505E1002005D005D905DB05D505EA05D905EA002E002005DE05E105DE05DB05D90020005000440046002005E905E005D505E605E805D5002005E005D905EA05E005D905DD002005DC05E405EA05D905D705D4002005D105D005DE05E605E205D505EA0020004100630072006F006200610074002005D5002D00410064006F00620065002000520065006100640065007200200035002E0030002005D505D205E805E105D005D505EA002005DE05EA05E705D305DE05D505EA002005D905D505EA05E8002E05D005DE05D905DD002005DC002D005000440046002F0058002D0033002C002005E205D905D905E005D5002005D105DE05D305E805D905DA002005DC05DE05E905EA05DE05E9002005E905DC0020004100630072006F006200610074002E002005DE05E105DE05DB05D90020005000440046002005E905E005D505E605E805D5002005E005D905EA05E005D905DD002005DC05E405EA05D905D705D4002005D105D005DE05E605E205D505EA0020004100630072006F006200610074002005D5002D00410064006F00620065002000520065006100640065007200200035002E0030002005D505D205E805E105D005D505EA002005DE05EA05E705D305DE05D505EA002005D905D505EA05E8002E>
/HRV (Za stvaranje Adobe PDF dokumenata najpogodnijih za visokokvalitetni ispis prije tiskanja koristite ove postavke. Stvoreni PDF dokumenti mogu se otvoriti Acrobat i Adobe Reader 5.0 i kasnijim verzijama.)
/HUN <FEFF004b0069007600e1006c00f30020006d0069006e0151007300e9006701710020006e0079006f006d00640061006900200065006c0151006b00e90073007a00ed007401510020006e0079006f006d00740061007400e100730068006f007a0020006c006500670069006e006b00e1006200620020006d0065006700660065006c0065006c0151002000410064006f00620065002000500044004600200064006f006b0075006d0065006e00740075006d006f006b0061007400200065007a0065006b006b0065006c0020006100200062006500e1006c006c00ed007400e10073006f006b006b0061006c0020006b00e90073007a00ed0074006800650074002e0020002000410020006c00e90074007200650068006f007a006f00740074002000500044004600200064006f006b0075006d0065006e00740075006d006f006b00200061007a0020004100630072006f006200610074002000e9007300200061007a002000410064006f00620065002000520065006100640065007200200035002e0030002c0020007600610067007900200061007a002000610074007400f3006c0020006b00e9007301510062006200690020007600650072007a006900f3006b006b0061006c0020006e00790069007400680061007400f3006b0020006d00650067002e>
/ITA <FEFF005500740069006c0069007a007a006100720065002000710075006500730074006500200069006d0070006f007300740061007a0069006f006e00690020007000650072002000630072006500610072006500200064006f00630075006d0065006e00740069002000410064006f00620065002000500044004600200070006900f900200061006400610074007400690020006100200075006e00610020007000720065007300740061006d0070006100200064006900200061006c007400610020007100750061006c0069007400e0002e0020004900200064006f00630075006d0065006e007400690020005000440046002000630072006500610074006900200070006f00730073006f006e006f0020006500730073006500720065002000610070006500720074006900200063006f006e0020004100630072006f00620061007400200065002000410064006f00620065002000520065006100640065007200200035002e003000200065002000760065007200730069006f006e006900200073007500630063006500730073006900760065002e>
/JPN <FEFF9ad854c18cea306a30d730ea30d730ec30b951fa529b7528002000410064006f0062006500200050004400460020658766f8306e4f5c6210306b4f7f75283057307e305930023053306e8a2d5b9a30674f5c62103055308c305f0020005000440046002030d530a130a430eb306f3001004100630072006f0062006100740020304a30883073002000410064006f00620065002000520065006100640065007200200035002e003000204ee5964d3067958b304f30533068304c3067304d307e305930023053306e8a2d5b9a306b306f30d530a930f330c8306e57cb30818fbc307f304c5fc59808306730593002>
/KOR <FEFFc7740020c124c815c7440020c0acc6a9d558c5ec0020ace0d488c9c80020c2dcd5d80020c778c1c4c5d00020ac00c7a50020c801d569d55c002000410064006f0062006500200050004400460020bb38c11cb97c0020c791c131d569b2c8b2e4002e0020c774b807ac8c0020c791c131b41c00200050004400460020bb38c11cb2940020004100630072006f0062006100740020bc0f002000410064006f00620065002000520065006100640065007200200035002e00300020c774c0c1c5d0c11c0020c5f40020c2180020c788c2b5b2c8b2e4002e>
/LTH <FEFF004e006100750064006f006b0069007400650020016100690075006f007300200070006100720061006d006500740072007500730020006e006f0072011700640061006d00690020006b0075007200740069002000410064006f00620065002000500044004600200064006f006b0075006d0065006e007400750073002c0020006b00750072006900650020006c0061006200690061007500730069006100690020007000720069007400610069006b007900740069002000610075006b01610074006f00730020006b006f006b007900620117007300200070006100720065006e006700740069006e00690061006d00200073007000610075007300640069006e0069006d00750069002e0020002000530075006b0075007200740069002000500044004600200064006f006b0075006d0065006e007400610069002000670061006c006900200062016b007400690020006100740069006400610072006f006d00690020004100630072006f006200610074002000690072002000410064006f00620065002000520065006100640065007200200035002e0030002000610072002000760117006c00650073006e0117006d00690073002000760065007200730069006a006f006d00690073002e>
/LVI <FEFF0049007a006d0061006e0074006f006a00690065007400200161006f00730020006900650073007400610074012b006a0075006d00750073002c0020006c0061006900200076006500690064006f00740075002000410064006f00620065002000500044004600200064006f006b0075006d0065006e007400750073002c0020006b006100730020006900720020012b00700061016100690020007000690065006d01130072006f00740069002000610075006700730074006100730020006b00760061006c0069007401010074006500730020007000690072006d007300690065007300700069006501610061006e006100730020006400720075006b00610069002e00200049007a0076006500690064006f006a006900650074002000500044004600200064006f006b0075006d0065006e007400750073002c0020006b006f002000760061007200200061007400760113007200740020006100720020004100630072006f00620061007400200075006e002000410064006f00620065002000520065006100640065007200200035002e0030002c0020006b0101002000610072012b00200074006f0020006a00610075006e0101006b0101006d002000760065007200730069006a0101006d002e>
/NLD (Gebruik deze instellingen om Adobe PDF-documenten te maken die zijn geoptimaliseerd voor prepress-afdrukken van hoge kwaliteit. De gemaakte PDF-documenten kunnen worden geopend met Acrobat en Adobe Reader 5.0 en hoger.)
/NOR <FEFF004200720075006b00200064006900730073006500200069006e006e007300740069006c006c0069006e00670065006e0065002000740069006c002000e50020006f0070007000720065007400740065002000410064006f006200650020005000440046002d0064006f006b0075006d0065006e00740065007200200073006f006d00200065007200200062006500730074002000650067006e0065007400200066006f00720020006600f80072007400720079006b006b0073007500740073006b00720069006600740020006100760020006800f800790020006b00760061006c0069007400650074002e0020005000440046002d0064006f006b0075006d0065006e00740065006e00650020006b0061006e002000e50070006e00650073002000690020004100630072006f00620061007400200065006c006c00650072002000410064006f00620065002000520065006100640065007200200035002e003000200065006c006c00650072002000730065006e006500720065002e>
/POL <FEFF0055007300740061007700690065006e0069006100200064006f002000740077006f0072007a0065006e0069006100200064006f006b0075006d0065006e007400f300770020005000440046002000700072007a0065007a006e00610063007a006f006e00790063006800200064006f002000770079006400720075006b00f30077002000770020007700790073006f006b00690065006a0020006a0061006b006f015b00630069002e002000200044006f006b0075006d0065006e0074007900200050004400460020006d006f017c006e00610020006f007400770069006500720061010700200077002000700072006f006700720061006d006900650020004100630072006f00620061007400200069002000410064006f00620065002000520065006100640065007200200035002e0030002000690020006e006f00770073007a0079006d002e>
/PTB <FEFF005500740069006c0069007a006500200065007300730061007300200063006f006e00660069006700750072006100e700f50065007300200064006500200066006f0072006d00610020006100200063007200690061007200200064006f00630075006d0065006e0074006f0073002000410064006f0062006500200050004400460020006d00610069007300200061006400650071007500610064006f00730020007000610072006100200070007200e9002d0069006d0070007200650073007300f50065007300200064006500200061006c007400610020007100750061006c00690064006100640065002e0020004f007300200064006f00630075006d0065006e0074006f00730020005000440046002000630072006900610064006f007300200070006f00640065006d0020007300650072002000610062006500720074006f007300200063006f006d0020006f0020004100630072006f006200610074002000650020006f002000410064006f00620065002000520065006100640065007200200035002e0030002000650020007600650072007300f50065007300200070006f00730074006500720069006f007200650073002e>
/RUM <FEFF005500740069006c0069007a00610163006900200061006300650073007400650020007300650074010300720069002000700065006e007400720075002000610020006300720065006100200064006f00630075006d0065006e00740065002000410064006f006200650020005000440046002000610064006500630076006100740065002000700065006e0074007200750020007400690070010300720069007200650061002000700072006500700072006500730073002000640065002000630061006c006900740061007400650020007300750070006500720069006f006100720103002e002000200044006f00630075006d0065006e00740065006c00650020005000440046002000630072006500610074006500200070006f00740020006600690020006400650073006300680069007300650020006300750020004100630072006f006200610074002c002000410064006f00620065002000520065006100640065007200200035002e00300020015f00690020007600650072007300690075006e0069006c006500200075006c0074006500720069006f006100720065002e>
/RUS <FEFF04180441043f043e043b044c04370443043904420435002004340430043d043d044b04350020043d0430044104420440043e0439043a043800200434043b044f00200441043e043704340430043d0438044f00200434043e043a0443043c0435043d0442043e0432002000410064006f006200650020005000440046002c0020043c0430043a04410438043c0430043b044c043d043e0020043f043e04340445043e0434044f04490438044500200434043b044f00200432044b0441043e043a043e043a0430044704350441044204320435043d043d043e0433043e00200434043e043f0435044704300442043d043e0433043e00200432044b0432043e04340430002e002000200421043e043704340430043d043d044b04350020005000440046002d0434043e043a0443043c0435043d0442044b0020043c043e0436043d043e0020043e0442043a0440044b043204300442044c002004410020043f043e043c043e0449044c044e0020004100630072006f00620061007400200438002000410064006f00620065002000520065006100640065007200200035002e00300020043800200431043e043b043504350020043f043e04370434043d043804450020043204350440044104380439002e>
/SKY <FEFF0054006900650074006f0020006e006100730074006100760065006e0069006100200070006f0075017e0069007400650020006e00610020007600790074007600e100720061006e0069006500200064006f006b0075006d0065006e0074006f0076002000410064006f006200650020005000440046002c0020006b0074006f007200e90020007300610020006e0061006a006c0065007001610069006500200068006f0064006900610020006e00610020006b00760061006c00690074006e00fa00200074006c0061010d00200061002000700072006500700072006500730073002e00200056007900740076006f00720065006e00e900200064006f006b0075006d0065006e007400790020005000440046002000620075006400650020006d006f017e006e00e90020006f00740076006f00720069016500200076002000700072006f006700720061006d006f006300680020004100630072006f00620061007400200061002000410064006f00620065002000520065006100640065007200200035002e0030002000610020006e006f0076016100ed00630068002e>
/SLV <FEFF005400650020006e006100730074006100760069007400760065002000750070006f0072006100620069007400650020007a00610020007500730074007600610072006a0061006e006a006500200064006f006b0075006d0065006e0074006f0076002000410064006f006200650020005000440046002c0020006b006900200073006f0020006e0061006a007000720069006d00650072006e0065006a016100690020007a00610020006b0061006b006f0076006f00730074006e006f0020007400690073006b0061006e006a00650020007300200070007200690070007200610076006f0020006e00610020007400690073006b002e00200020005500730074007600610072006a0065006e006500200064006f006b0075006d0065006e0074006500200050004400460020006a00650020006d006f0067006f010d00650020006f0064007000720065007400690020007a0020004100630072006f00620061007400200069006e002000410064006f00620065002000520065006100640065007200200035002e003000200069006e0020006e006f00760065006a01610069006d002e>
/SUO <FEFF004b00e40079007400e40020006e00e40069007400e4002000610073006500740075006b007300690061002c0020006b0075006e0020006c0075006f00740020006c00e400680069006e006e00e4002000760061006100740069007600610061006e0020007000610069006e006100740075006b00730065006e002000760061006c006d0069007300740065006c00750074007900f6006800f6006e00200073006f00700069007600690061002000410064006f0062006500200050004400460020002d0064006f006b0075006d0065006e007400740065006a0061002e0020004c0075006f0064007500740020005000440046002d0064006f006b0075006d0065006e00740069007400200076006f0069006400610061006e0020006100760061007400610020004100630072006f0062006100740069006c006c00610020006a0061002000410064006f00620065002000520065006100640065007200200035002e0030003a006c006c00610020006a006100200075007500640065006d006d0069006c006c0061002e>
/SVE <FEFF0041006e007600e4006e00640020006400650020006800e4007200200069006e0073007400e4006c006c006e0069006e006700610072006e00610020006f006d002000640075002000760069006c006c00200073006b006100700061002000410064006f006200650020005000440046002d0064006f006b0075006d0065006e007400200073006f006d002000e400720020006c00e4006d0070006c0069006700610020006600f60072002000700072006500700072006500730073002d007500740073006b00720069006600740020006d006500640020006800f600670020006b00760061006c0069007400650074002e002000200053006b006100700061006400650020005000440046002d0064006f006b0075006d0065006e00740020006b0061006e002000f600700070006e00610073002000690020004100630072006f0062006100740020006f00630068002000410064006f00620065002000520065006100640065007200200035002e00300020006f00630068002000730065006e006100720065002e>
/TUR <FEFF005900fc006b00730065006b0020006b0061006c006900740065006c0069002000f6006e002000790061007a006401310072006d00610020006200610073006b013100730131006e006100200065006e0020006900790069002000750079006100620069006c006500630065006b002000410064006f006200650020005000440046002000620065006c00670065006c0065007200690020006f006c0075015f007400750072006d0061006b0020006900e70069006e00200062007500200061007900610072006c0061007201310020006b0075006c006c0061006e0131006e002e00200020004f006c0075015f0074007500720075006c0061006e0020005000440046002000620065006c00670065006c0065007200690020004100630072006f006200610074002000760065002000410064006f00620065002000520065006100640065007200200035002e003000200076006500200073006f006e0072006100730131006e00640061006b00690020007300fc007200fc006d006c00650072006c00650020006100e70131006c006100620069006c00690072002e>
/UKR <FEFF04120438043a043e0440043804410442043e043204430439044204350020044604560020043f043004400430043c043504420440043800200434043b044f0020044104420432043e04400435043d043d044f00200434043e043a0443043c0435043d044204560432002000410064006f006200650020005000440046002c0020044f043a04560020043d04300439043a04400430044904350020043f045604340445043e0434044f0442044c00200434043b044f0020043204380441043e043a043e044f043a04560441043d043e0433043e0020043f0435044004350434043404400443043a043e0432043e0433043e0020043404400443043a0443002e00200020042104420432043e04400435043d045600200434043e043a0443043c0435043d0442043800200050004400460020043c043e0436043d04300020043204560434043a0440043804420438002004430020004100630072006f006200610074002004420430002000410064006f00620065002000520065006100640065007200200035002e0030002004300431043e0020043f04560437043d04560448043e04570020043204350440044104560457002e>
/ENU (Use these settings to create Adobe PDF documents best suited for high-quality prepress printing. Created PDF documents can be opened with Acrobat and Adobe Reader 5.0 and later.)
>>
/Namespace [
(Adobe)
(Common)
(1.0)
]
/OtherNamespaces [
<<
/AsReaderSpreads false
/CropImagesToFrames true
/ErrorControl /WarnAndContinue
/FlattenerIgnoreSpreadOverrides false
/IncludeGuidesGrids false
/IncludeNonPrinting false
/IncludeSlug false
/Namespace [
(Adobe)
(InDesign)
(4.0)
]
/OmitPlacedBitmaps false
/OmitPlacedEPS false
/OmitPlacedPDF false
/SimulateOverprint /Legacy
>>
<<
/AddBleedMarks false
/AddColorBars false
/AddCropMarks false
/AddPageInfo false
/AddRegMarks false
/ConvertColors /ConvertToCMYK
/DestinationProfileName ()
/DestinationProfileSelector /DocumentCMYK
/Downsample16BitImages true
/FlattenerPreset <<
/PresetSelector /MediumResolution
>>
/FormElements false
/GenerateStructure false
/IncludeBookmarks false
/IncludeHyperlinks false
/IncludeInteractive false
/IncludeLayers false
/IncludeProfiles false
/MultimediaHandling /UseObjectSettings
/Namespace [
(Adobe)
(CreativeSuite)
(2.0)
]
/PDFXOutputIntentProfileSelector /DocumentCMYK
/PreserveEditing true
/UntaggedCMYKHandling /LeaveUntagged
/UntaggedRGBHandling /UseDocumentProfile
/UseDocumentBleed false
>>
]
>> setdistillerparams
<<
/HWResolution [2400 2400]
/PageSize [612.000 792.000]
>> setpagedevice
|
| id | nasplib_isofts_kiev_ua-123456789-83170 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 0130-5395 |
| language | English |
| last_indexed | 2025-12-07T17:50:43Z |
| publishDate | 2013 |
| publisher | Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України |
| record_format | dspace |
| spelling | Letichevsky, A. Letichevskyi, A. Weigert, T. Peschanenko, V. 2015-06-16T14:12:04Z 2015-06-16T14:12:04Z 2013 Satisfiability For Symbolic Verification in VRS / A. Letichevsky, A. Letichevskyi, T. Weigert, V. Peschanenko // Управляющие системы и машины. — 2013. — № 3. — С. 81-87. — Бібліогр.: 26 назв. — англ. 0130-5395 https://nasplib.isofts.kiev.ua/handle/123456789/83170 519.686.2 Рассмотрены использование логики первого порядка в символьной верификации спецификаций требований программного обеспечения, символьные модели систем, которые есть транзиционными системами с символьными состояниями представленных формулой логики первого порядка. Использованы методы Satisfiability Modulo Theory вместо логического вывода в соответствующем исчислении для эффективных вычислений в предикатных трансформерах. This paper demonstrates the use of the first order logic in symbolic verification of the requirement specifications of reactive software systems. We consider symbolic models of a specified system which are transition systems with symbolic states represented by formulae of the first order logic. To efficiently compute predicate transformers the Satisfiability Modulo Theory methods are used instead of the logical inference in the corresponding calculi. Розглянуто використання логіки першого порядку у символьній верифікації специфікацій вимог програмного забезпечення, символьні моделі систем, які є транзиційними системами з символьними станами представленими формулою логіки першого порядку. Використано методи Satisfiability Modulo Theory замість логічного виводу у відповідних численнях для ефективного обчислення у предикатних трансформерах. en Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України Управляющие системы и машины Информационные технологии и системы Satisfiability For Symbolic Verification in VRS Выполнимость для символьной верификации VRS Здійсненість для символьної верифікації VRS Article published earlier |
| spellingShingle | Satisfiability For Symbolic Verification in VRS Letichevsky, A. Letichevskyi, A. Weigert, T. Peschanenko, V. Информационные технологии и системы |
| title | Satisfiability For Symbolic Verification in VRS |
| title_alt | Выполнимость для символьной верификации VRS Здійсненість для символьної верифікації VRS |
| title_full | Satisfiability For Symbolic Verification in VRS |
| title_fullStr | Satisfiability For Symbolic Verification in VRS |
| title_full_unstemmed | Satisfiability For Symbolic Verification in VRS |
| title_short | Satisfiability For Symbolic Verification in VRS |
| title_sort | satisfiability for symbolic verification in vrs |
| topic | Информационные технологии и системы |
| topic_facet | Информационные технологии и системы |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/83170 |
| work_keys_str_mv | AT letichevskya satisfiabilityforsymbolicverificationinvrs AT letichevskyia satisfiabilityforsymbolicverificationinvrs AT weigertt satisfiabilityforsymbolicverificationinvrs AT peschanenkov satisfiabilityforsymbolicverificationinvrs AT letichevskya vypolnimostʹdlâsimvolʹnoiverifikaciivrs AT letichevskyia vypolnimostʹdlâsimvolʹnoiverifikaciivrs AT weigertt vypolnimostʹdlâsimvolʹnoiverifikaciivrs AT peschanenkov vypolnimostʹdlâsimvolʹnoiverifikaciivrs AT letichevskya zdíisnenístʹdlâsimvolʹnoíverifíkacíívrs AT letichevskyia zdíisnenístʹdlâsimvolʹnoíverifíkacíívrs AT weigertt zdíisnenístʹdlâsimvolʹnoíverifíkacíívrs AT peschanenkov zdíisnenístʹdlâsimvolʹnoíverifíkacíívrs |