Insertion modeling in distributed system design
The paper describes insertion modeling methodology, its implementation and applications. Insertion modeling is a methodology of model driven distributed system design. It is based on the model of interaction of agents and environments [1-2] and use Basic Protocol Specification Language (BPSL) for...
Saved in:
| Date: | 2008 |
|---|---|
| Main Authors: | , , , , , , |
| Format: | Article |
| Language: | English |
| Published: |
Інститут програмних систем НАН України
2008
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/2599 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Insertion modeling in distributed system design / A.A. Letichevsky, J.V. Kapitonova, V.P. Kotlyarov, A.A. Letichevsky Jr., N.S. Nikitchenko, V.A. Volkov, T. Weigert // Проблеми програмування. — 2008. — № 4. — С. 13-38. — Бібліогр.: 28 назв. — англ. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1859830303123570688 |
|---|---|
| author | Letichevsky, A.A. Kapitonova, J.V. Letichevsky Jr, A.A. Kotlyarov, V.P. Nikitchenko, N.S. Volkov, V.A. Weigert, T. |
| author_facet | Letichevsky, A.A. Kapitonova, J.V. Letichevsky Jr, A.A. Kotlyarov, V.P. Nikitchenko, N.S. Volkov, V.A. Weigert, T. |
| citation_txt | Insertion modeling in distributed system design / A.A. Letichevsky, J.V. Kapitonova, V.P. Kotlyarov, A.A. Letichevsky Jr., N.S. Nikitchenko, V.A. Volkov, T. Weigert // Проблеми програмування. — 2008. — № 4. — С. 13-38. — Бібліогр.: 28 назв. — англ. |
| collection | DSpace DC |
| description | The paper describes insertion modeling methodology, its implementation and applications. Insertion modeling is a
methodology of model driven distributed system design. It is based on the model of interaction of agents and environments
[1-2] and use Basic Protocol Specification Language (BPSL) for the representation of requirement specifications
of distributed systems [3-6]. The central notion of this language is the notion of basic protocol – a sequencing
diagram with pre- and postconditions, logic formulas interpreted by environment description. Semantics
of BPSL allows concrete and abstract models on different levels of abstraction. Models defined by Basic Protocol
Specifications (BPS) can be used for verification of requirement specifications as well as for generation of test
cases for testing products, developed on the basis of BPS.
Insertion modeling is supported by the system VRS (Verification of Requirement Specifications), developed for
Motorola by Kiev VRS group in cooperation with Motorola GSG Russia. The system provides static requirement
checking on the base of automatic theorem proving, symbolic and deductive model checking, and generation of
traces for testing with different coverage criteria. All tools have been developed on a base of formal semantics of
BPSL constructed according to insertion modeling methodology.
The VRS has been successfully applied to a number of industrial projects from different domains including Telecommunications,
Telematics and real time applications.----------------
Стаття описує методологію інсерційного моделювання, її реалізацію та застосування. Інсерційне моделювання являє собою методологію проектування розподілених систем, що управляється моделлю. Ця методологія базується на теорії взаємодіючих агентів та середовищ [1-2] та використовує Basic Protocol Specification Language (BPSL) для представлення специфікацій вимог до розподілених систем. [3-6]. Діаграма Послідовності з пре- та постумовами (логічними формулами, що інтерпретуються відповідно до опису середовища) – Базовий Протокол є центральним поняттям цієї мови. Семантика BPSL дозволяє конкретні та абстракті моделі рівних рівнів абстрактності. Моделі визначені як Basic Protocol Specifications (BPS) можуть у подальшому бути використані як для верифікація специфікацій вимог та і для генерації тестових наборів.
Інсерційне моделювання підтримується системою VRS (Verification of Requirement Specifications), створеною для компанії Моторола київською групою VRS у співробітництві із ЗАТ Моторола-Санкт-Петербург. Система дозволяє статичний аналіз вимог на основі автоматичного доведення теорем, символьної та дедуктивної перевірки моделей та породження трас для тестування із заданими критеріями покриття. Всі засоби були розроблені на базі формальної семантики BPSL, побудованої відповідно до методології інсерційного моделювання VRS була успішно застосована у великій кількості індустріальних проектів із різних галузей, включаючи телекомунікації, телематику та системи реального часу.----------------
Статья описывает методологию инсерционного моделирования, ее реализацию и применения. Инсерционное моделирование представляет собой методологию проектирования распределенных систем, управляемых[ моделью. Эта методология базируется на теории взаимодействующих агентов и сред [1-2] и использует Basic Protocol Specification Language (BPSL) для представления спецификаций требований к распределенным системам. [3-6]. Диаграма Последовательности с пред- и пост-условиями (логическими формулами, интерпретируемыми соответственно описания среды), называемая Базовый Протокол, – центральное понятие этого языка. Семантика BPSL позволяет конкретные и абстрактные модели разных уровней абстрактности. Модели заданные Basic Protocol Specifications (BPS) могут в дальнейшем быть использованы как для верификации спецификаций требований так и для генерации тестовых наборов.
Инсерционное моделирование поддерживается системой VRS (Verification of Requirement Specifications), созданной для компании Моторола киевской группой VRS в сотрудничестве с ЗАО Моторола-Санкт-Петербург. Система позволяет статический анализ требований на основе автоматического доказательства теорем, символьной и дедуктивной проверки моделей и порождения трасс для тестирования с заданными критериями покрытия. Всеі средства были разработаны на базе формальной семантики BPSL, построенной соответственно методологии инсерционного моделирования.
VRS была успешно применена в большом количестве индустриальных проектов из разных областей, включая телекоммуникации, телематику и системы реального времени.
|
| first_indexed | 2025-12-07T15:31:39Z |
| format | Article |
| fulltext |
Теоретичні та методологічні основи програмування
© A.A. Letichevsky, J.V. Kapitonova, V.P. Kotlyarov, A.A. Letichevsky Jr., N.S.Nikitchenko,
V.A. Volkov, and T.Weigert, 2008
ISSN 1727-4907. Проблеми програмування. 2008. № 4 13
UDC 623/518.3/517.5
A.A. Letichevsky, J.V. Kapitonova , V.P. Kotlyarov, A.A. Letichevsky Jr., N.S.Nikitchenko,
V.A. Volkov, and T.Weigert
INSERTION MODELING IN DISTRIBUTED SYSTEM DESIGN
The paper describes insertion modeling methodology, its implementation and applications. Insertion modeling is a
methodology of model driven distributed system design. It is based on the model of interaction of agents and envi-
ronments [1-2] and use Basic Protocol Specification Language (BPSL) for the representation of requirement speci-
fications of distributed systems [3-6]. The central notion of this language is the notion of basic protocol – a se-
quencing diagram with pre- and postconditions, logic formulas interpreted by environment description. Semantics
of BPSL allows concrete and abstract models on different levels of abstraction. Models defined by Basic Protocol
Specifications (BPS) can be used for verification of requirement specifications as well as for generation of test
cases for testing products, developed on the basis of BPS.
Insertion modeling is supported by the system VRS (Verification of Requirement Specifications), developed for
Motorola by Kiev VRS group in cooperation with Motorola GSG Russia. The system provides static requirement
checking on the base of automatic theorem proving, symbolic and deductive model checking, and generation of
traces for testing with different coverage criteria. All tools have been developed on a base of formal semantics of
BPSL constructed according to insertion modeling methodology.
The VRS has been successfully applied to a number of industrial projects from different domains including Tele-
communications, Telematics and real time applications.
Introduction
Insertion modeling is the technology
of system design founded on the theory of
interaction of agents and environments. This
theory has been developed in [1–2]. It is
based on process algebra and is intended for
the unification of different models of interac-
tion and computation (such as CCS, CSP, π-
calculus, mobile ambients etc.). In the last
years this approach has been successfully ap-
plied to the problems of the verification of
requirement specifications [3–5] for distrib-
uted concurrent systems from different sub-
ject domains including Telecommunications,
Telematics, distributed computing and others.
These applications are supported by the sys-
tem VRS developed for Motorola by Kiev
VRS group. In combination with TAT system
developed in Motorola Software Group Rus-
sia it supports also the generation of test cases
from requirement specifications.
We use the basic protocol specifica-
tions [4–6] to formalize requirement specifi-
cations for distributed concurrent systems.
Basic protocols are parameterized MSCs
(Message Sequence Charts) with pre- and
postconditions interpreted on the states of an
environment with inserted agents. Semanti-
cally basic protocol can be considered as a
statement )( βα >→<∀ ux of some kind of
dynamic logic. In this statement x is a (typed)
list of parameters, α and β are precondition
and postcondition, correspondingly, and u is a
process defined by the MSC diagram. Pre-
conditions and postconditions are formulas of
first order multisorted language called the Ba-
sic Language. This language is used to de-
scribe the properties of the states of a system
represented as a composition of environment
and agents inserted into this environment. The
evolving part of a system is represented by
distinguished functional and predicate sym-
bols from the signature of the basic language
called the attributes of an environment. The
process u describes finite behavior of an envi-
ronment with inserted agents. When parame-
ters of a basic protocol are fixed, then we can
speak about instantiated basic protocol.
The purpose of this paper is to repre-
sent the formal definitions of the main con-
cepts of the Basic Protocols Specification
Language (BPSL), define the notion of im-
plementation of Basic Protocols Specifica-
tions (BPS) and to give the high level de-
scription of the tools of the VRS system. Each
Теоретичні та методологічні основи програмування
14
BPS consists of two parts: the environment
description and the set of basic protocols. En-
vironment description determines the signa-
ture of basic language and the restrictions on
possible interpretations of this signature
(some part of a signature can be interpreted at
the very beginning, for example, numerical
functions and predicates, or constructors for
the states of agents). The signature can also
include some constructors for actions of
agents inserted into environment. The set of
basic protocols defines the requirements to
the behavior of a system and implicitly
defines the insertion function for the given
environment. The requirements informally
can be expressed in the following way: If the
precondition of some instantiated protocol is
valid and the process of this protocol started
then after successful termination of this
process the postcondition is valid.
The semantics of BPS is defined by
the variety of possible implementations of
BPS that satisfy the informal property above.
On abstract level an implementation is repre-
sented as an attributed transition system, that
is a labeled transition system with transitions
labeled by actions and states labeled by at-
tribute labels.
We distinguish among concrete and
abstract implementations. A concrete imple-
mentation assumes the concrete interpretation
of a signature of basic language, and the states
of concrete implementations are labeled by
the attribute valuations that are the partial
mappings from constant attribute expressions
(expressions of a type ,...),( 21 aaf where f is
an attribute symbol and ,..., 21 aa are constant
terms of corresponding types) to their values.
Each closed (no free variables) formula of ba-
sic language has the value on each state of a
concrete implementation. Basic protocols can
be also considered as formulas, but formulas
of dynamic logic that express the main be-
havioral requirements. These formulas must
be valid on any state of a concrete implemen-
tation and arbitrary values of parameters. Also
we would like to specify concrete implemen-
tations for a case of concurrent performance
of several basic protocols. To catch the situa-
tion the permutability relation for attributed
actions is added to BPS and is used for the
definition of so called partially sequential
composition of processes. For empty permu-
tability relation this composition coincides
with sequential composition and for the case
when all actions are permutable it is a parallel
composition.
For abstract implementations we do
not use concrete interpretation of a basic lan-
guage mentioned above. An abstract imple-
mentation of BPS is defined as an attributed
transition system with validity relation be-
tween the attribute labels and the formulas of
the basic language. Abstract and concrete im-
plementations are partially ordered by two
abstraction relations: direct and inverse. These
relations were studied in [6]. They generalize
many abstractions referred to in [8-9] and
were used for the definition of two abstract
implementations of a system of basic proto-
cols that cover concrete implementations. The
first one is used for the verification, the sec-
ond one – for generating of tests.
The main tools of the VRS system are
divided into two groups: static tools and dy-
namic tools. Static tools include checkers for
consistency and completeness of precondi-
tions, safety checker, time checker and anno-
tation checker. All these tools are based on
deductive system, which contains the univer-
sal prover for the first order predicate calculus
and special provers for linear numeric arith-
metic (over real numbers and integers), enu-
merated and symbolic data types. Deductive
system is capable for extension by integrating
new specialized provers and solvers for spe-
cial theories.
Dynamic tools include concrete and
symbolic trace generators (CTG and STG).
Both are assigned for simulating the behavior
of models of a system defined by BPS by
generating their traces in the system state
space. For CTG the state space is generated in
a traditional way by the valuation of attrib-
utes. The generation of traces is controlled by
the goal state condition, safety conditions
checked along traces, and some other means
and heuristics that bound the search space.
The states for STG are symbolic. Like as in
symbolic model checking they are defined by
logic formulas and symbolic computations in
Теоретичні та методологічні основи програмування
15
combination with deduction are used for
computing transitions. The BPS used for con-
crete trace generation can be used for sym-
bolic trace generation as well.
The paper is structured as follows.
First we give the general introduction to in-
sertion modeling based on the model of inter-
action of agents and environments and de-
scribe the environments for MSC. Then the
main features of the Basic Protocol Specifi-
cation Language are described. The semantics
of this language for concrete and abstract im-
plementations are defined and used then for
the definition of requirements for CTG and its
high level description. Then we describe the
main algorithms used for the static require-
ments checking. After the high level descrip-
tion of STG we define the notion of abstrac-
tion and prove the theorem about the connec-
tion between concrete and abstract imple-
mentations. We also describe some tools for
tests generation. The last section contains the
conclusions and the comparison with related
approaches.
Insertion modeling
Insertion modeling is the development
and investigation of distributed concurrent
systems by means of representing them as a
composition of interacting agents and envi-
ronments. Both agents and environments are
attributed transition systems, considered up to
bisimilarity, but environments are additionally
provided with insertion function used for the
composition and characterizing the behavior
of environment with inserted agents. Attrib-
uted transition systems are labeled transition
systems such that besides the labels of transi-
tions called actions, they have states labeled
by attribute labels. If s is a state of a system,
then its attributed label will be denoted as
al(s). A transition system can be also enriched
by distinguishing in its set of states S the set
of initial states SS ⊆0 and the set of terminal
states SS ⊆∆ . For attributed transition sys-
tem we use the following notation.
ss a ′′→ :: αα means that there is a transi-
tion from the state s with attributed label
L∈α to the state s΄ labeled by attributed la-
bel L∈′α , and this transition is labeled by
action Aa ∈ . Therefore an enriched attrib-
uted system S can be considered as a tuple
>→××⊆< ∆ LSSASTSSLAS :al,,,,,, 0
A pair >< LA, of actions and attributed la-
bels is called the signature of a system S. We
also distinguish a hidden action τ and hidden
attributed label 1. In the difference from other
actions and attributed labels these hidden la-
bels are not observable.
Behaviors. Each state of a transition
system is characterized up to bisimilarity by
its behavior represented as an element of be-
havior algebra (a special kind of a process al-
gebra). The behavior of a system in a given
state for the ordinary (labeled, but not attri-
buted) systems is specified as an element of a
complete algebra of behaviors F(A) (with pre-
fixing a.u, non-deterministic choice u+v,
constants 0, ∆ , ⊥ , the approximation relation
, and the lowest upper bounds of directed sets
of behaviors) [2]. In the sequel we shall use
the term process as a synonym of behavior.
For attributed systems attributed be-
haviors should be considered as invariants of
bisimilarity. The algebra >< LAU ,, of attrib-
uted behaviors is constructed as a three sorted
algebra. The main set is a set U of attributed
behaviors, A is a set of actions, L is a set of
attribute labels. Prefixing and non-determi-
nistic choice are defined as usual (nondeter-
ministic choice is associative, commutative,
and idempotent). Besides the usual behavior
constants 0 (deadlock), ∆ (successful
termination) and ⊥ (undefined behavior), the
empty action τ is also introduced with the
identity
uu =.τ
The operation Uu ∈):(α of labeling the be-
havior Uu ∈ with an attribute label L∈α is
added. The empty attribute label 1 is intro-
duced with the identity
uu =:1
The approximation is extended to labeled be-
haviors so that
vuvu ):( ):( <∧=⇔< βαβα .
Constructing a complete algebra
F(A,L) of labeled behaviors is similar to the
constructing the algebra F(A). Each behavior
u in this algebra has a canonical form:
Теоретичні та методологічні основи програмування
16
u
Jj
jj
Ii
ii uauu εα ++= ∑∑
∈∈
.: ,
where τα ≠≠ ji a,1 , uε is a termination con-
stant ( ⊥+∆⊥∆ ,,,0 ), all summands are
different and behaviors iu and ju are in the
same canonical form.
Behaviors, i.e., elements of the algebra
F(A,L) can be considered as the states of an
attributed transition system. The transition
relation of this system is defined as follows:
uu
uua
uvuvu
uvua
a
a
:::
.:
:):(:1:
.
ββα
α
ααα
τ
τ
→
→
→+=+
→+
.
A set E of behaviors is called transi-
tion closed if EuuuEu a ∈′⇒′→∈ , .
Ordinary labeled transition systems
are considered as a special case of attributed
ones with the set of attribute labels equal to
{1}, and the algebra F(A) is identified with
F(A,{1}).
Insertion function. Environment
>< ϕ,,,,, MALCE is defined as a transition
closed set of behaviors ),( LCFE ⊆ with in-
sertion function EMAFE →× ),(:ϕ . The
only requirement for insertion function is that
it must be continuous w.r.t. approximation
relations defined on E and F(A,M). Usually
the behaviors of environment are represented
by the states of a transition system consider-
ing them up to bisimilarity. The state ),( ueϕ
of an environment resulting after agent inser-
tion (identified with the corresponding be-
havior) is denoted as ][ue or ][ueϕ to men-
tion insertion function explicitly, and the it-
eration of insertion function
as ]]...)[])[[(...(],...,,[ 2121 mm uuueuuue = . Envi-
ronments can be considered as agents and
therefore can be inserted into a higher level
environments with another insertion func-
tions, so the state of multilevel environments
can be described for example by the following
expression: ,...],...],[,...],,[[ 2
2
1
2
22
1
1
1
1 uueuuee ψψϕ .
The most of insertion functions considered in
this paper are one-step or head insertion func-
tions. Typical rules for the definition of inser-
tion function are the following (one-step in-
sertion):
,
][][
,
ueue
uuee
c
aa
′′→
′→′→
(1)
.
][][ ueue
ee
c
c
′→
′→
(2)
The first rule can be treated as
follows. Agent u ask for permission to
perform an action a, and if there exist an a-
transition from the state e the performance of
a is allowed and both agent and environment
come to the next state with observable action
c of environment. The second rule describes
the move of environment with suspended
move of an agent. The additivity conditions
usually are used:
][][][ veuevue +=+ ,
][][])[( ufueufe +=+ .
The rules (1–2) can be also written in the
form of rewriting rules:
fuecuaea +′′=′′ ][.].)[.( ,
guecuec +′=′ ][.])[.( .
MSC environment. The standard se-
mantics of MSC diagrams is defined as pro-
cess algebra semantics [7–8], so that the mea-
ning of MSC is the set of traces of a process
over the set of events used in MSC. The pro-
cess algebra proposed by M.A.Reniers for this
purpose was very complicated and far from
implementations. An alternative approach has
been developed in [9–10] where insertion se-
mantics of MSC has been defined. The main
difference from the Reniers semantics is that
we consider branching time instead of linear
and synchronizing treatment of conditions and
references. We shall use this semantics as
intermediate semantics for basic protocols so
let us consider it here.
Теоретичні та методологічні основи програмування
17
send message (i: m to j)
receive message (i: m from j)
local action (i: action b)
instance start (i: instance)
instance stop (i: stop)
condition (J: condition y)
local condition (i: cond y(J))
Fig. 1
We use in basic protocols only simple
MSC, that is MSC with the following con-
structs: instances, conditions, messages, core-
gions, and local actions. Before inserting
MSC B to the MSC-environment it is con-
verted to the process nppBproc ||...||)( 1=
where npp ,...,1 are sequential compositions
of events corresponding to the instances of a
diagram (parallel composition must be used
for coregions) in the same order as on in-
stances. Events are considered as actions and
these actions are message actions, local ac-
tions, instance actions and local conditions
used instead of ordinary conditions sharing
several instances. Parallel composition is de-
fined by means of interleaving. We use the
notations for events as in [9] (fig.1).
The process over the actions listed in
this figure is called MSC-process and MSC-
process without local conditions is called re-
duced MSC process.
For example, if B is a diagram of fig.2,
then proc(B)=((b:instance).(b:cond
y{b,c}).(b:m to c). (b:n to c).(b:cond
z{b,c}).(b:stop) ||
(c:instance).(c:cond y{b,c}).(c:m from b). (c:n
from b).(c:cond z{b,c}).(c:stop)).
The state of MSC-environment is a
triple of functions e = (Ο, Σ, Υ) (empty envi-
ronment, no inserted agents) or the expression
],...,,[ 21 muuue , where e is an empty environ-
ment and agents muuu ,...,, 21 are MSC-proc-
esses. The states of MSC environment are
unlabeled. The function Ο is a partial function
of three arguments m, i, j, where m is a mes-
sage expression, and i and j are instances.
This function yields values in the set of non-
negative integers. Equation Ο(m, i, j) = k
means that earlier k message events (i : m to j)
occurred for which there are no corresponding
receiving message events pending. Function Σ
is a partial function of two arguments y and J.
The first argument is a condition expression,
the second is a set of instances. The value Σ(y,
J) represents a nonempty subset of the set J.
Σ(y, J) = I means that earlier a control event i
: cond y(J) had been executed, for all in-
stances Ji ∈ . The condition event is attached
to all instances in J, and Σ(y, J) is the set of all
instances which have already been synchro-
nized by the condition y. The last component
Υ of a triple is a set of all instances that had
already started. This explanation results in the
following definition of environment transi-
tions. For empty environment e a transition
ee a ′→
is possible in the following cases:
1. a = (i: m to j),
1),,(.),,(., +=′∈ jimejimei ΟΟΥ
2. a = (i: m from j),
1),,(.),,(., −=′∈ jimejimei ΟΟΥ
3. a = (i: action b), ee =′
4. a = (i: instance), }{.. iee ∪=′ ΥΥ
5. a = (i: stop), }{\.. iee ΥΥ =′
c b
y
m
n
z
Fig.2
Теоретичні та методологічні основи програмування
18
6. a = (i: cond y(J)),
)),, cond:(.,(), cond:(., iJyieJJyieJ ΣΣΥ Φ=′⊆
where
}{),,(
)},{\,(
}{),,(
iIiIJ
iiJJ
iiJ
∪=Φ
=⊥Φ
=⊥Φ
and a rule is applied if previous one is not
applied. In all these rules only the
components of environment state that change
their value are shown. All other components
of environment left unchanged. Now we
define the rule (1) for empty MSC-
environment so that in the cases 1-3 ac = , in
cases 4-5 τ=c , and in the case 6, c = (J:
condition y) if =⊥′ ), cond:(. Jyie Σ and
τ=c otherwise.
Initial state of empty MSC environ-
ment is ),,(0 ∅⊥⊥=e where the first two
components are nowhere defined functions
and the last component is the empty set of in-
stances. For the process B on fig. 2 the repre-
sentation of the process ][0 Be is given on
fig. 3.
To define insertion function for non-
empty environment let us define some auxil-
iary notions. MSC-process is called belonging
to instance i if all its actions belong to the in-
stance i. MSC-process is called decomposable
if it can be represented as a parallel composi-
tion of processes belonging to different in-
stances. The set of all decomposable proc-
esses is transition closed (follows directly
from the definition).
The process proc(B) is equivalent to
the instance oriented textual representation of
MSCs and we can define the composition u*v
of decomposable MSC-processes which in the
case of MSCs is equivalent to their vertical
product. This composition is defined by the
following identities:
),||||);(||...||);((
)||||...||(*)||||...||(
11
11
SQqpqp
SqqQpp
mm
mm
=
=
where mpp ,...,1 belong to the same instances
as mqq ,...,1 , correspondingly, Q and S have
no common instances. Note that joining two
instances we can use the identity ((i: stop).
(i: instance)) = ∆, because these two behav-
iors are insertion equivalent.
For nonempty environment e[u] and
decomposable processes u and v define
][],[ vuevue ∗= . This definition can be ex-
tended to arbitrary number of decomposable
processes:
][0 Be = (
((b:instance). (c:instance)+(c:instance). (b:instance)); {b,c}:condition y);
(b:m to c). 1e [
(b:n to c). (b:cond z{b,c}).(b:stop) ||
(c:m from b). (c:n from b).(c:cond z{b,c}).(c:stop)
]
) = (
((b:instance). (c:instance)+(c:instance). (b:instance));
({b,c}:condition y). (b:m to c).(
((b:n to c). (c:m from b)+(c:m from b). (b:n to c));
(c:n from b).({b,c}:condition z);
((b:stop). (c:stop) +(c:stop).(b:stop));
][0 ∆e
)
)
Fig. 3
Теоретичні та методологічні основи програмування
19
]...[],...,[ 11 mm uueuue ∗∗= .
To use this definition for arbitrary (not only
decomposable) MSC-processes one must ex-
tend the notion of the composition of MSC-
processes.
Partially sequential composition of
behaviors. Let us consider attributed behav-
iors of the algebra F(A,L). Let
},|:{: AaLaAL ∈∈= αα be the set of
attributed actions (unlabeled actions are 1:a,
attribute labels are τα : ). First we define the
permutability relation over the set L:A. This is
an arbitrary symmetric and reflexive binary
relation denoted as ba ↔ . Intuitively this
relation means that )*(~)*( abba E for envi-
ronment E where the agents from F(A,L) will
be inserted into. We say that an attributed ac-
tion a:α is reachable from behavior u if
there exists behavior v such that v:α is
reachable from u and vv a ′→:α . Let us
expand the permutability relation of attributed
actions to attributed behaviors. We say that
behaviors u and v are permutable ( vu ↔ ) if 0
and ⊥ are not reachable from u and v, and for
each attributed action a reachable from u and
attributed action b reachable from v ba ↔ .
Now we can define the partially se-
quential composition vu ∗ of two behaviors.
Let u and v are two attributed behaviors, rep-
resented in the canonical form:
v
Ll
ll
Kk
kk
u
Jj
jj
Ii
ii
vbv
vuauu
εβ
εα
++=
=++=
∑∑
∑∑
∈∈
∈∈
.:
,.:
Then
);().()(:
).()(:
,,
vu
Llbu
ll
Kku
kk
Jj
ij
Ii
ii
lk
vubvu
vuavuvu
εεβ
α
β
+∗+∗+
+∗+∗=∗
∑∑
∑∑
∈↔∈↔
∈∈
A sequential composition of termination con-
stants is defined with the following relations:
0);0( ,);( ,);( ==⊥⊥=∆ εεεε .
Note that partially sequential composition is
not continuous with respect to the first argu-
ment; however it is continuous with respect to
the second one. It is also continuous with re-
spect to both arguments, if the first argument
is finite and totally defined. Let now u and v
be completely unlabelled. Then if all actions
are permutable, then a partially sequential
composition coincides with a parallel compo-
sition, and if no actions are permutable, then
we obtain a sequential composition of behav-
iors. The notion of partially sequential com-
position originates from the notion of weak
sequential composition introduced by Renier
for describing the semantics of MSC
diagrams and is a generalization of the latter
(for not delayed nondeterministic choice).
Permutability for MSC-environ-
ment. The states of MSC have no attribute
labels (the empty label is omitted). Two ac-
tions are permutable if they belong to differ-
ent instances, or in the case of conditions
(sharing a set of instances) have no common
instances. Now we can define partially se-
quential composition of arbitrary (not neces-
sarily decomposable) MSC-processes and de-
fine for them insertion function as above but
changing vertical product to partially sequen-
tial composition that coincides with vertical
product for decomposable processes.
For MSCs B and C we have
proc(B)*proc(C)=proc(B*C) where the prod-
uct of MSCs is their vertical product. If 0e is
the initial state of empty MSC-environment
and B is an MSC diagram then [B] denotes the
behavior of a system )]([0 Bproce .
Interpreted MSC. MSC environment
regulates the correct ordering of MSC-actions
in MSC-processes. The actions of interpreted
MSCs can also define the data transformation
in higher level data environment D. Transi-
tions dd a ′→ in D for MSC action a define
the corresponding transformation. The inser-
tion function for data environment can be de-
fined in the same way as for MSC environ-
ment using partially sequential composition,
but with another notion of permutability. Be-
low several kinds of data environments will
be considered. For MSC diagram B we can
construct MSC-process [B] and insert this
process into data environment obtaining two
level environment d[[B]]. As it was men-
tioned before d[[B],[C]]= d[[B]*[C]] =
d[[B*C]].
Basic protocol specifications
Let us start with a very simple and
well known example: readers and writers
Теоретичні та методологічні основи програмування
20
(R&W). The environment keeps shared record
that can be sent to readers and updated by
writers. Readers and
writers are two types of agents that can be in-
serted into this environment. Basic Protocol
Specification (BPS) of a system consists of
two parts: environment description and the set
of basic protocols. Environment description
has a text representation and basic protocols
are MSC diagrams with pre- and postcondi-
tions. The description of R&W environment
is presented in fig.4. It shows that there are
two environment attributes rec of symbolic
type and queue, the list of symbolic type data.
Each reader has two Boolean attributes regis-
tered and access allowed. The agents of a
type writer have no attributes in the environ-
ment. Safety condition asserts that access (to
the rec) is allowed only for registered readers.
This is a dynamic requirement which must be
satisfied in any environment state. The last
assumption states that initially there are no
registered readers (and therefore access is not
allowed for all of them). Other sections of
environment description will be discussed
later.
The set of basic protocols represents
the set of local requirements to the system.
Each protocol is a simple MSC with a special
text block with parameters. Only two condi-
tions are allowed in Basic Protocol. The first
one is at the beginning of MSC. It is shared
by all instances of the protocol and contains a
precondition formula as a condition text. The
second condition is at the end of a protocol, it
is shared by all instances and contains a post-
condition as a text. Text block contains a list
of typed parameters used for instantiation of a
protocol.
Basic protocols for R&W are repre-
sented in figures 5-7. Each diagram is accom-
panied by its name and a list of parameters.
First three protocols describe the local be-
havior of the system inspired by reader activ-
ity. The protocol write(m,s,x) describes the
activity of the writer, and the last protocol up-
date(x,t) describes the transition of the envi-
ronment (without agents participation). The
first four protocols have an expression of a
type ),( smτ where τ is a type of agent and s
is the state expression. It is a state assumption
and means that the agent m of the type τ is in
a state s. Agents are represented by their
unique names (ids), states are represented by
means of behavior (process) algebra expres-
sions.
environment(
agent types:(
reader: (
registered: Bool,
access allowed: Bool
),
writer: Nil
);
attributes:(
rec: symb,
queue: list of symb
);
safety condition: Forall(m:reader)(
m.access allowed->m.registered
);
initial condition:(
Forall(m:reader)(
~(reader m.registered)&
~(reader m.access allowed)
)
)
);
Fig. 4
Теоретичні та методологічні основи програмування
21
reader m
env m
reader(m, release.s)&
reader m.registered
reader(m, s)&
~(reader m.registered)
ok
release(m,s)
writer m
env queue
writer(m, write x.s)
writer(m, s)&
add_to_tail(queue,(m:x))
write(m:x)
ok
write(m,s,x)
Fig. 6
reader m
env m
reader(m, register.s)&
~(reader m.registered)
reader(m, s)&
reader m.registered
register m
ok
register(m,s)
reader m
env m
reader(m, read.s)&
reader m.access allowed
reader(m, s)&
~(reader m.access allowed)
read m
rec
read(m,s)
Fig. 5
Теоретичні та методологічні основи програмування
22
Therefore the symbols register, read,
and release are reader actions, and write is a
writer action. The actions of environment are
send and receive message events or local ac-
tions presented by MSC. Agent attributes are
accessed by the expressions of the type xm. τ ,
where τ is the type of agent m and x is the
name of attribute (type of agent can be omit-
ted in some cases). The instances are named
by expressions containing the names of agents
or the name of environment env possibly at-
tached by the list of attributes or the names of
agents.
In symbolic notation a basic protocol
will be represented by expressions of the form
)( βα >→<∀ ux
where x is a list of parameters, α and β are
precondition and postcondition, correspond-
ingly, and u is an MSC process (usually in-
serted to MSC environment).
Basic language used for pre- and
postconditions is the first order language of
multi-sorted predicate calculus with equality.
The signature of this language has predefined
part and the part defined by an environment
description. Predefined part contains simple
numeric types int and real, with arithmetical
operations and inequalities, Boolean type
Bool, type agent state with operations of
process algebra (prefixing and nondetermin-
istic choice), symbolic type symb with some
predefined constructors (such as (():()), ((),())
etc.), and composite types: arrays and lists of
simple type elements and functional types
τττ →),...,( 1 m where mττ ,...,1 are already
defined types and τ is a simple type. However
there are some restrictions on the use of func-
tional types for different tools. For example,
concrete trace generator allows only enumer-
ated types for mττ ,...,1 .
Predefined part of basic language sig-
nature contains also the agent state function
symbol τstate for each agent type τ defined
env rec
update x
update(x,t)
Fig. 7
(queue=t)&(rec=x)&
Forall(n:reader)(n.registered->
n.access allowed)
(queue=(x,t))&
Exist(n:reader)(n.registered)&
Forall(n:reader)(n.registered->
~(n.access allowed))
env queue
Теоретичні та методологічні основи програмування
23
in environment description. This is a unary
symbol for the function of a type
stateagent nameagent → . These symbols are
used implicitly in state assumption expres-
sions ),( smτ equivalent to formulas
smstate =)(τ . Some constant symbols for
agent states can also be included into the sig-
nature of basic language an can be defined by
behavior algebra equations. These equations
can be represented in reductions section of
environment description. For example, possi-
ble equations for the behaviors of readers and
writers in R&W example are:
state reduction: rs(x)(
reader init = register.(loop read;release),
writer init = (loop write;release),
loop x = (x;(loop x+Delta))
).
This is a correct behavior of readers and writ-
ers. More free behavior including incorrect
activity can be described by another reduc-
tions:
incorrect state reduction: rs()(
reader init = register state + read state +
+ release state,
register state = register. reader init,
read state = read. reader init,
release state = release. reader init,
writer init = write state + writer release,
write state = write. writer init,
writer release = release. writer init
).
In environment description one can
define several enumerated types in the section
types (for example types: (colour: (red,
green, yellow), size: (small, big),…)). One
can also define agent types with associated
agent attributes that are considered as func-
tional symbols. Functional and array
attributes have arity more then 0, attributes of
simple types and lists (simple attributes) are
considered as functional symbols of arity 0.
They are equivalent to the variables that
change their values when a system moves
from one state to another (but they cannot be
bounded by quantifiers). Other attributes can
also change their values during the evolution
of a system, but this changing may refer only
to the change of the parts of a value.
Universal and existential quantifiers
with variables typed by simple types can be
used in formulas. All terms in formulas must
have simple types.
The difference of precondition and
postcondition is that in postcondition one can
use the imperative elements like assignments.
In this case assignment (x:=y) is equivalent to
the statement: new value of attribute x (after
performing a basic protocol) is equal to the
previous value of the expression y (before
performing of a protocol). In protocol
write(m,s,x) the operator add_to_tail
(queue,(m:x)) is used. This operator adds new
element to a list and is interpreted as state-
ments so that new value of list queue is the
result of performing of the operator
add_to_tail applied to the previous value of
the second parameter.
The signature of basic language may
include also abstract data types defined in the
sections types, functions, axioms, and
reductions. Section types contains symbols
for simple abstract data types, section
functions contains specification of functional
symbols of type τττ →),...,( 1 m , axioms are
first order formulas without attributes, and
reductions are systems of rewriting rules that
must define canonical forms.
This information is used by deductive
system, which contains a universal procedure
for the first order theory, and procedures for
eliminating quantifiers and solving equations
in special theories (numeric, symbolic and
enumerated) and some distinguished data
types theories.
Semantics of BPS
In [4] semantics of basic protocols has been
presented in a very abstract and general form.
In [6] there were introduced two kinds of se-
mantics, direct and inverse, and a theorem
about connection between abstract and con-
crete implementations of a system of basic
protocols was formulated with a sketch of
proof. Here we shall consider more concrete
definitions close to processes represented by
MSCs and the implementation in VRS sys-
tem. Moreover we use here the independent
notion of implementation of BPS and the con-
structions of [4] and [6] can be now proved to
be implementations.
Теоретичні та методологічні основи програмування
24
As in [4] and [6] we associate a tran-
sition systems with each BPS as its possible
semantic values and distinguish between con-
crete and abstract implementations. In con-
crete implementations all functional and
predicate symbols are interpreted on corre-
sponding domains and the state of environ-
ment is the partial valuation defined on all at-
tributes. In abstract implementations the class
of possible interpretations for the signature is
fixed, and the states of environment are for-
mulas of basic language.
Implementation of BPS. First we
should answer the question: what is the im-
plementation of a basic protocol specification.
Then the class of all possible implementations
will be declared as a semantic value of BPS.
It must be an attributed transition system with
validity relation α=|s where s is a state and
α is a closed statement (no free variables) of
basic language. The transitions of this system
must be labeled by environment actions that
are the events of basic protocols considered as
MSCs.
The validity relation |= must satisfy
the following condition. Let T be the set of
formulas of basic language that includes all
axioms of the environment description (in-
cluding reductions) and all true statements of
the specialized theories for interpreted part of
a signature. Then the set C(s) of all statements
α valid in s, that is statements for which
α=|s is valid, must be closed relative to the
inference in the theory T, that is for any
statement )(sC∈α all statements β such
that βα −|,T are also in C(s). The set C(s)
relates to the observable part of a system and
must depend only on the attribute label of a
state s. In abstract form of a system model the
attribute label can be identified with this set,
but in practice more constructive representa-
tions are used.
Note that basic language includes all
information about the types and independent
behaviors of agents to be inserted into their
environment. But they interact with environ-
ment only via basic protocols (state assump-
tions) and can be present implicitly. Some in-
formation about the variety of agents can be
represented by means of validity relation
which can include more statements except of
deduced in the theory T.
If a system S is the implementation of
BPS it must satisfy the following requirement.
Let B is an instantiated basic protocol (a pro-
tocol with substituted parameters) with pre-
condition α and postcondition β . Let
Ss ∈ . Then
βα =′⇒′→= |,| ][ ssss B
.
This requirement is not enough because it
does not take into account the possibility of
concurrent performing of several protocols.
To make this possible we use corresponding
permutability relation and partially sequential
composition. The modified requirement can
now be expressed in the following form:
)3(|,| ][][ βα =′⇒′ →= ∗ ssss CB
for arbitrary MSC C such that ][][ CB ↔ .
Therefore to define the notion of implemen-
tation we must define the permutability rela-
tion for basic protocol specifications.
A system S can be considered as a
data environment for reduced MSC processes
defined by equation (1), additivity conditions,
and equation
s[u,v] = s[u*v].
Let us consider some assumptions about in-
terpretation of MSC actions on S, that is a
transition relation for S. We assume that mes-
sage and local actions as well as instance ac-
tions do not change the set C(s). It means that
if ss a ′→ and a is not a condition, then
C(s) = C(s΄). We introduce two kinds of con-
ditions: condition when and condition set to
distinguish the performance of pre- and
postconditions. Condition a = (J: condition
when y) is a guard, it does not change the att-
ribute labels of the states of S, but allows the
transition ss a ′→ only if s|=y. Condition
set changes not only the state of S but also its
validity relation. If a = (J: :condition set y)
and ss a ′→ then ys =′ | . Assume that in
basic protocols preconditions are changed to
when condition and postconditions are chan-
ged to set condition. The set of MSC actions
modified in this way will be called the modi-
fied MSC action set. A BPS is called con-
sistent if a theory T defined by environment
description is consistent and the conjunction
of all initial conditions and safety conditions
is satisfiable.
Теоретичні та методологічні основи програмування
25
Summarizing discussion above we
give the following definition of implementa-
tion of BPS. An attributed transition system
S over the set of modified MSC actions is
called an implementation of a given consistent
BPS if
1. Validity relation |= depending only on
attribute labels and closed over the theory T,
defined by environment description, is de-
fined on S.
2. A permutability relation is defined on
the set of modified attributed MSC actions so
that condition (3) held for all basic protocols.
Trivial implementation consisting with
only one deadlock state always exists. So
usually we are interested in the existence of
nontrivial implementations, for example free
of dead locks or satisfying safety (integrity)
conditions or satisfying other kinds of dy-
namic properties.
Direct and inverse implementations.
The difference between two kinds of imple-
mentations is in the applicability condition
used in the formula (3). In this formula the
applicability condition is α=|s for instantia-
ted precondition α . This is a direct
implementation. For inverse implementation a
dual condition is used: )|( α¬=¬ s . This con-
dition means that precondition α is con-
sistent with current state and is weaker than
direct condition. For concrete implementati-
ons these conditions coincide (consistency
and completeness of concrete implementa-
tion), so this is interesting first of all for abs-
tract implementations. Considered form of
representation of inverse applicability condi-
tion is difficult for computations so simpler
conditions are used in practice. For example,
let attributed labels are formulas of basic lan-
guage. Then αα =⇔= |)(| ss alT, . Let
,...),(,...),,()( 2121 rrrrs ααγ ==al , where
,..., 21 rr attributes occurring in two formulas
and they are simple attributes. Then sufficient
condition for inverse applicability can be ex-
pressed in the form
,...)),(,...),(,...)(,(| 212121 xxxxxxs αγ ∧∃= .
Concrete and abstract implementations
Concrete implementations. Concrete
implementations of BPS are characterized
first of all that a concrete interpretation of all
symbols from the signature of the base lan-
guage are defined for them, except for attrib-
utes. For them only the value domains and the
ranges of the arguments are defined. Another
characteristic of concrete implementations is
an explicit representation of the system in the
form of a composition of the environment and
agents inserted into it. Finally, a concrete im-
plementation should be deterministic with re-
spect to the agents’ behavior. In other words,
an arbitrary change of the state of the agents
and their attributes should lead to a uniquely
determined change of other attributes of the
environment. Here a certain class of concrete
implementations will be described.
BPS assumed to be consistent for a fi-
nite number of agents. That is the set of axi-
oms is consistent and there exists an initial
state of environment with finite number of
agents satisfying initial and safety conditions.
State s of empty environment is the partial
valuation of the set of all attributes. To
achieve the determinism some additional hid-
den attributes can be added to the attributes
described in environment description together
with rules or algorithms for their change. Let
A be the set of all attributes (including hidden
ones), that is a set of all constant attribute ex-
pressions ,...),( 21 aaf where f is an attribute
symbol and ,..., 21 aa are constant terms of
corresponding types. If f is a symbol of agent
attribute it has the form (m.x) where m is the
name of agent and x is the name of attribute.
In this case we write ,...),(. 21 aaxm . We add
an undefined value ⊥ to all domains and con-
sider the state s as a totally defined mapping
DA →:s where D is the union of all do-
mains extended by undefined value. Let 0A
be the set of all attributes defined by envi-
ronment description (they are observable).
Define an attribute label for s as a narrowing
of s to 0A , that is
00 ),())((,:)( AalDAal ∈=→ xxsxss . Let
Eq(s) is the conjunction of all equalities
0),( A∈= xxsx . Define validity relation so
that ⇔= α|s α=|)(, sEqT . In the most of
applications when quantifiers are restricted by
finite sets of values (agent names or enumer-
ated types) and s is defined only on the finite
Теоретичні та методологічні основи програмування
26
set of attributes the validity of the formulas of
basic language is computed without any de-
duction simply by substituting the values.
The next step of constructing the concrete
implementation is the definition of transitions
for the empty environment. Define ss a ′→
so that
1. If a is not a condition, then
)()( ss ′= alal ;
2. If a = (J: condition when y),
)()( ss ′= alal and ys =| ;
3. If a = (J: condition set y), then ys =′ |
and only those attributes which are the
left hand sides of assignments or occur
in logic formulas can change their val-
ues in the new state.
Now define the states of entire system as
]:,...,:][...[ 111 nnm uuqqs νν∗∗
where mqqq ∗∗= ...1 is the partially sequen-
tial composition of MSCs with modified ac-
tion sets and inserted into MSC environment,
nuu ,...,1 are the states of agents over the ac-
tion set A, nνν ,...,1 are their names (all differ-
ent) considered as the attribute labels of
agents. Transitions of named agents are de-
fined as follows:
vmumvu aa :: →⇒→
Initial state
]:,...,:][[ 11 kk wws µµ∆
is such that all initial and safety conditions are
valid on s. So the set S of empty environment
states is considered as an environment for in-
terpreted MSC agents and the set s[q] is con-
sidered as an environment for agents over A
with insertion function defined below. We
call this environment as the main one. We as-
sume that the set of named agents that can be
inserted into the main environment is fixed
and constitutes only the agents in the initial
state. This assumption will be used each time
the protocol is instantiated or the value of
quantifier formula with variables bounded to
the agent states or names is computed.
The permutability relation for MSC
agents is defined in the following way.
1. Unconditional actions are per-
mutable if they belong to different instances;
2. Conditional actions a and b are
permutable if their instance sets do not inter-
sect and for all states s if ss ba ′→ . and
ss ab ′′→ . then )()( ss ′′=′ alal .
From this definition it follows that for
two MSCs A and B such that ][][ BA ↔ from
ss BA ′ → ][*][ and ss AB ′′ → ][*][ it follows
that )()( ss ′′=′ alal .
The insertion function for the entire
system is assumed to be additive and satisfy
the commutativity condition:
],][[],][[ uvqsvuqs = . Also we assume that
⇒′′→ ][][ qsqs a ]][[]][[ uqsuqs a ′′→ and
]][[],:][[ vqsvmqs =∆ . We say that an agent
m participate in q if a formula ),( umτ occur
in q. We also assume that the type of an agent
is uniquely defined by its name m. Now we
can define the insertion function by means of
the following transition rules.
Changing the state of a protocol:
where action a is supposed to be uncondi-
tional action.
Activating a protocol b:
,
][]:,...,:][[
,,.],|
11 pqsumumqs
ssaqpabs
a
kk
a
∗′→
′→↔== [ α
(5)
where )when condition :( αJa = ,
kk umum :,...,: 11 are agents involved into the
protocol b (their state assumptions occur in
the condition α ). The protocol b is assumed
to be instantiated by constant values of pa-
rameters.
Terminating a protocol:
.
]:,...,:][[][
,
11 kk
a
aa
umumqsqs
qqss
′′→
′→′→
(6)
Here q is a partially sequential composition of
MSC agents, a is a condition set action (there-
fore a modified postcondition), kmm ,...,1 are
the names of agents which participate in q,
but do not participate in q′ , kuu ,...,1 are their
states. The new states of agents are defined
syntactically by state assumptions from post-
condition.
The described implementation is direct one.
The inverse implementation can work when
some attributes needed for computing validity
relation have no values. This is normal for
,
][][
,
qsqs
qqss
a
aa
′′→
′→′→
(4)
Теоретичні та методологічні основи програмування
27
abstract implementations used for proving
properties but is not normal for concrete im-
plementations for which the undefined value
usually is the indication of error.
Denote the class of concrete imple-
mentations of BPS P described in this section
as Concr(P)
Theorem 1. Each transition system S
from the class Concr(P) is a direct and inverse
implementation of P.
The first property of implementation
follows from the definition of validity relation
for S, the second property follows from the
definition of permutability relation. For con-
crete implementation we have a concrete in-
terpretation of the theory T. Therefore for
each state s each formula α is valid ( α=|s )
or not valid ( α¬=|s ). Therefore
)|(| αα ¬=¬⇔= ss and the each direct im-
plementation from Concr(P) is at the same
time the inverse implementation and wise
versa.
Abstract implementations. For ab-
stract implementations the interpretation of
the signature of a basic language is not strictly
defined and the validity relation is derived
from attributed labels of states and a theory T
defined by environment description (includ-
ing predefined interpretation). We assume that
the attributed labels of the states Ss ∈ of
empty environment are formulas of the basic
language and the validity set
}|)(|{)( αα −= ss alT,C . The environment
for abstract implementation is constructed in
the same way as a concrete two level envi-
ronment. The low level is the environment for
basic protocols and the high level is the level
for named agents over the action set A. So the
general state of a system has the form
]:,...,:][...[ 111 nnm uuqqs νν∗∗ ,
but in the difference from concrete imple-
mentations the agents occurring in the state do
not constitute a complete set of agents in the
system. New agents can appear and disappear
during the performance of environment and
their states can be defined by means of sym-
bolic expressions.
Instantiation of basic protocols in the
case of concrete and abstract implementations
are different, however in the both cases the
solution of the precondition must be found,
that is the list of values of parameters such
that after substitution the precondition is
valid. In the case of concrete implementation
the solution must be concrete, and in the case
of abstract implementation the solution can
use symbolic values in the extended signature
of basic language. For example, let precondi-
tion be the formula ax ≤ where x is an inte-
ger parameter and a is a simple integer attrib-
ute. If the value of a is defined then concrete
implementation can select arbitrary integer
less or equal to a for x (which one depends on
hidden computations with hidden attributes.
Otherwise the protocol is not applicable. In
the case of direct abstract implementation a
new symbolic value z for x can be introduced
as a new constant symbol and a condition
)( az ≤ will be added to the attribute label of
a current state if ≠⊥a is valid. The permuta-
bility relation is defined in the same way as
for concrete interpretation.
The insertion function for abstract im-
plementations is defined by means of the
same rules (4–6) as for concrete implementa-
tions with slight change and another restric-
tions on the constituents of these rules. The
rule (4) is used without any changes because
the unconditional actions never change the
attributed labels. The rule (5) for activating
protocol is slightly changed. To explain this
change let us consider the symbolic represen-
tation of a protocol b:
))()()(( xxuxx βα >→<∀
Applicability of this protocol in the current
state s:γ is equivalent to the condi-
tion )(|, xxαγ ∃=T . If this condition is valid,
we can found a general solution
),...(),( 2211 ztxztx == for the problem
)(|, xαγ =T , where ,...),( 21 zzz = is the list of
symbolic parameters needed to express the
general solution. Their symbols must be dif-
ferent from all other symbols already used in
BPS and have corresponding types. In the
worst case if there are no good solution pro-
cedure, the list x can be renamed to new pa-
rameters list z and )(zα added to the attrib-
uted label. Let
,...),()),(when condition :()( 21 tttxJxa == α .
Then the modified rule (5) can be represented
as follows:
Теоретичні та методологічні основи програмування
28
The process of instantiation of a basic proto-
col which could be hidden in the case of con-
crete basic protocols because there were no
symbolic parameters, must be defined explic-
itly together with the rule of activation of a
protocol. Another peculiarity of symbolic
case is that not all agents participating in the
residual part p(t) of a protocol are taken from
the list of inserted in the current moment
agents but some can be generated in the
moment of instantiation. For example, some
of parameters from the list z can be the names
of new agents, others can be parameters of
their state expressions in the state
assumptions. All this depends on the states of
a system and algorithms used for the
implementation. One more peculiarity of
symbolic implementations is that it can
implement inverse implementation model. In
this case the activation rule must looks as
follows.
The termination rule is the same as for conc-
rete implementation, but let us present it with
the explicit change of attributed labels:
]:,...,:][[][
),:():(
11 kk
a
aa
umumqsqs
qqss
′′→
′→′′→ γγ
(6a)
Here )set condition :( βJa = , and the attrib-
uted label γ ′ must satisfy the condition com-
mon for all condition set actions: the postcon-
dition must be valid on s′′ :γ that is
βγ →′−|T . The function ),( βγγ spt=′ is
called a predicate transformer in the state s.
As for concrete implementation
kmm ,...,1 are the names of agents which par-
ticipate in q, but do not participate in q′ ,
kuu ,...,1 are their states. Again the new states
of agents are defined syntactically by state
assumptions from postcondition, but the list
of agents can be not complete, some agents
can disappear or even all of them disappear
(k = 0).
Predicate transformers. Two classes
of implementations are described in a very
general way. They contains a big undefined
components that depend on subject domain,
the not formalized requirements, and concrete
circumstances of the development process. A
source BPS model can be very concrete and
remains no choices for implementation details
or too abstract and provides a big freedom in
making decisions. The definition of termina-
tion rule has the most indefinite component.
Any condition γ ′ consistent with the theory T
and strengthening β can be chosen for attrib-
uted label of new state of environment. We
can make the choice of predicate transformer
more definite if some additional requirements
are added to it. For example, we can claim
that in arbitrary concrete implementation cov-
ered by the given abstract implementation the
values of attributes can change only if they
occur in postcondition. In this case if
...2211 ∨∧∨∧= δγδγγ and ,..., 21 δδ have
no occurrences of the attributes occurring in
β , we can set βδδβγ ∧∨∨= ...)(),( 21pt .
Denote the class of direct (inverse) ab-
stract implementations of BPS P described in
this section as Adir(P) (Ainv(P)).
Theorem 2. Each system from the
class Adir(P) (Ainv(P)) is a direct (inverse)
implementation of P.
The validity relation is closed by defi-
nition. The second property of implementa-
tion follows from the definition of permuta-
bility.
Abstractions. As it is clear from
above that the implementations can have dif-
ferent levels of abstraction. This notion can
be defined exactly in terms of attributed tran-
sition systems with validity relation consid-
ered up to bisimilarity. The definition below
)]()[:))(((]:,...,:][[
:))((),(),().(]),(|):(
)(
11
)(
tpqstumumqs
ststaqxpxabxxs
ta
kk
ta
∗′∧→
′∧→↔=∃=
αγ
αγαγ [
(5a)
)]()[:))(((]:,...,:][[
:))((),(),().(])),(|):((
)(
11
)(
tpqstumumqs
ststaqxpxabxxs
ta
kk
ta
∗′∧→
′∧→↔=¬∃=¬
αγ
αγαγ [
(5b)
Теоретичні та методологічні основи програмування
29
is close to the definition of [6] but does not
use the labeled actions. First we must intro-
duce some simplification of transition systems
connected with elimination of hidden transi-
tions, that is transitions labeled by τ .
Hidden transitions of the form
ss ′→ : 1: 1 τ are called redundant. All
redundant transitions may be eliminated in the
following way: first, add transitions according
to the rules:
,
:
: ,: 1: 1
,
,: 1: 1
ss
ssss
ss
ssss
a
a
′′→
′′→′′→
′′→
′′→′′→
α
α
τ
ττ
τ
where 1≠α , until it is possible (an infinite
number of steps may be required, at each step
all rules are applied to all states simultane-
ously), then all redundant transitions are eli-
minated. After such transformation at least
one state in each hidden transition will be la-
beled by attributed label different of 1. The
system with no redundant transitions is called
reduced. Below only reduced systems will be
considered.
Let S and S ′ be two attributed (not
necessarily different) systems with the same
signatures, validity relations and the same ba-
sic language denoted as BL. Define the ab-
straction relation SS ′×⊆Abs in such a way
that
))|()|)(((),( ααα =′⇒=∈∀⇔∈′ ssss BLAbs
.
To denote abstraction relations (the state s is
an abstraction of the state s′ ) the notation
ss ′< will be used instead of Abs∈′),( ss .
If ss ′< and ss <′ , then the states s and s′
are called deductively equivalent.
The system S is called a direct ab-
straction (or a direct abstract model) of the
system S ′ and the system S ′ is called a con-
cretization of the system S if there exists a
relation 1−⊆ Absϕ , which is a relation of
modeling (simulation). It means, that the fol-
lowing statement holds:
)).),()((
),)((,(
ϕ
ϕ
∈′∧′→′′∈′∃⇒
⇒→∧∈′′∈′∈∀
tttsSt
tsssSsSs
a
a
The system S is called an inverse abstraction
(or an inverse abstract model) of the system
S ′ and the system S ′ is called an inverse
concretization of the system S if there exists a
relation 1−⊆ Absϕ , which is a relation of in-
verse modeling. It means, that the following
statement holds:
)).),()((
),)((,(
ϕ
ϕ
∈′∧→∈∃⇒
⇒′→′∧∈′′∈′∈∀
tttsSt
tsssSsSs
a
a
For enriched systems the requirement of pre-
serving the initial and terminal states is added
in both cases: if )(0 ∆′′∈′ SSs and ϕ∈′ ),( ss ,
then )(0 ∆∈ SSs .
The system and its abstraction are re-
lated in the following way. If from an ab-
straction of some initial system state a certain
property is reachable in its direct abstraction,
then it is also reachable from the initial sys-
tem state. For inverse abstraction the inverse
property hold: if from initial state of a system
some property is reachable then it is reachable
from some initial state of its inverse abstrac-
tion.
Let us consider as a famous example a
Kripke system S ′ ; i.e., an attributed system
with binary attributes nxx ,...,1 . The states of
this system are labelled with Boolean func-
tions of the variables nxx ,...,1 . Let
),...,( 1 nxxf be one of such functions. Let us
decompose it with respect to the first k vari-
ables; i.e., present it in the form:
),,...,,,...,(...
),...,(
111
1
1
nkkk
n
xxfxx
xxf
k
+∨=
=
αααα
where the disjunction is over all binary vec-
tors ),...,( 1 kαα such that
),...,,,...,( 11 nkk xxf +αα is different from 0.
Let us define the transformation
),...,()),...,(( 11,...,1 knxx xxgxxfP
k
= of the
function ),...,( 1 nxxf , by:
k
kk xxxxg αα ...),...,( 1
11 ∨= .
Let us modify the system S ′ by substituting
the function al for its labeling function al΄
with ))(la()(al ,...,1
sPs
kxx ′= . Denoting thus
modified system as S, we shall receive and
abstract model of the system S ′ . Similar
models are used in model checking to reduce
the state space generated for checking.
The importance of the notion of ab-
straction is explained by the following theo-
rem.
Теоретичні та методологічні основи програмування
30
Theorem 3. Each abstract
implementation of the class Adir(P) (Ainv(P))
is an abstraction of some concrete implemen-
tation from the class Concr(P). This follows
from the well known logic fact that each con-
sistent axiom system has a consistent com-
plete interpretation.
Theorem 4. There exist a direct and
an inverse abstract implementations which are
direct and inverse abstractions of all imple-
mentations from Concr(P).
Corresponding constructions were de-
fined in the paper [6]. Complete proof need
some more mathematics and we are going to
this in the next papers.
Concrete trace generator
Purpose. CTG module of VRS system
provide checking the reachability of proper-
ties, detecting deadlocks, non-determinisms,
safety violations, unreachable requirements,
usage of uninitialized attributes and admitted
range attribute overflow on a base of a con-
crete model of formal requirement specifica-
tion in the form of BPS. The problems above
are solved by means of generating traces
reachable from the initial state of a model.
The generated traces can be also used for test
generation. Results are represented in
.MSC/PR and .txt formats.
In general, the CTG module input is the set of
the following files:
• Environment description;
• Filters description;
• Events description;
• Set of Basic Protocols.
Environment. Environment descrip-
tion is restricted to the following elements:
list of enumerated types in type description,
list of environment attributes, list of agent ty-
pes, list of instances, initial values of listed
above elements and agent states. Abstract
syntax of environment description is as fol-
lows:
<environment descr>::= environment(
types: <enumerated types
declaration>;
attributes: <list of attr descr>;
agent_types: <list of agent descr>;
agents: <list of typed agent ids>;
instances: <list of instances>;
initial: env(
(
attributes: <list of environment
attributes values>;
agent_parameters: <list of
agent attributes values>
),
<agent states>
)
).
Enumerated type declaration defines
the symbol of enumerated type and the set of
its values. Attribute description defines the
symbol of environment attribute and its type.
Agent type description defines the name of an
agent type and the list of agent attributes for
this type together with the types of these at-
tributes. The names of agents inserted into
environment are represented in the list of
typed agents ids. The list of instances repre-
sents the set of instances which can be used in
MSC diagrams representing the interaction
activity of agents. There is no explicit corre-
spondence between agents and instances.
Usually each instance corresponds to one
agent, but there can be another kinds of cor-
respondence (one instance – several agents or
one agent – several instances). Some of the
instances can be used to represent the activity
of environment. This correspondence does not
explicitly expressed in the model and is in the
mind of a user.
Every environment/agent attribute has
one of the following types: integer, real, enu-
merated, symbolic type, list, array, functional
type (parameterized attributes) with only
enumerated parameters and values.
Environment description represents
the structure of environment and contains
some information about agents inserted into
this environment. It also defines the initial
state of environment. In this definition each
agent and environment attribute can be as-
signed a value. Default is the undefined value.
The initial states of all agents are represented
in <agent states>.
Теоретичні та методологічні основи програмування
31
Filters. Filters are used for the restric-
tion of the set of traces generated by CTG.
The following filters are available in CTG:
goal state,
restricted state ,
break state,
safety conditions.
All filters are defined by formulas
checked during the trace generation.
Goal state defines the successful ter-
mination of generating procedure. It is used to
check the reachability of goal state condition
or generating testing sequences for given cov-
erage criteria.
Restricted states cut the set of states
used for the search of goal states. When the
restricted state is reached the system returns
back to the nearest choice point.
Break states switch the trace generator
to interactive mode. In this mode the direction
of further development of traces is selected by
user. After several steps of interactive move a
user can return to automatic generation of
traces.
Safety conditions must be true at any
states so it is checked each time the system
comes into the new state. If some of the safety
conditions is violated the generation is
stopped and the corresponding trace is fixed.
There are also some other restrictions
like the maximal trace length or switching the
control of visited states.
There are also some predefined condi-
tions such as deadlock condition, non-deter-
minisms, unreachable requirements, usage of
uninitialized attributes and admitted range at-
tribute overflow which are checked and result
terminating the generation of a trace when
these conditions are valid.
Events description contains the in-
formation about messages used in MSC dia-
grams: message names, parameters of mes-
sages, parameter values.
Basic protocols. To be efficient the
CTG allows a very restricted class of basic
protocols. Each protocol has the following
abstract syntax form in symbolic notation:
)),(&),(),(
),(&)(&),()(,(Forall
yxAyxvyxB
yxFxuyxLyx
>→<
→
In this formula ,...),( 21 xxx = is a list of pa-
rameters called key agent parameters. They
are used in the conjunction of state assump-
tions u(x). The first state assumption in u(x) is
called a key agent assumption and has the
form ,...)),(,( 21 zzsmτ where m is the name of
a key agent and can be one of the key agent
parameters, s is the (constant) name of an
agent state, and ,..., 21 zz are all other key
agent parameters. All other agent state as-
sumptions do not contain parameters and are
constructed with symbolic constants, agent
parameters, and attributes. The list
,...),( 21 yyy = contains data parameters that
obtain their values from the definitions
...)&&(),( 2211 tytyyxL === , the right
hand sides of these definitions can depend on
key agent parameters, but not on data ones.
The formula F(x,y) is the formula of basic
language. It can contain quantifiers but only
for finite sets represented by enumerated data
types. The expression v(x,y) is a conjunction
of agent state assumptions for agents intro-
duced by precondition and A(x,y) is the con-
junction of imperative statements: assign-
ments, list processing statements
(add_to_head, add_to_tail etc.). B(x,y) is
MSC representation of this basic protocol.
The restrictions on basic protocols
structure show that the performance of basic
protocols can be done by computation on the
current state of a system under modeling. The
state expression in key agent assumption is
matched with the states of all agents to get the
values of parameters x and to decide which of
the agents can be used as a key agent in the
performance of the protocol. Data parameters
obtain their values after the choice of a key
agent and are used for instantiating the proto-
col by means of substitution.
The main part of precondition is a
logic formula F(x,y) which is computed on
the current state if it is possible. The failure
can appear if the values of some of the
attributes needed for computation are
undefined. So if precondition is valid the
protocol can be applied by performing the
imperative statements of postcondition in
parallel (first compute the right hand sides of
assignments then assign). The state
assumptions in postcondition give the new
states of agents participating in the protocol.
Expressions in pre- and postconditions use
various functions defined on data types. Some
Теоретичні та методологічні основи програмування
32
other imperative constructions in addition to
assignments are admissible in the postcondi-
tions.
Generating traces. Ordinary trace for
a transition system is a sequence
n
aaa sss n→→→ −121 ...21
of conjugated transitions. If restrict only to
observable part of a trace it is a sequence
121 ,...,, −naaa , and for attributed systems an
observable trace is
)(al...)(al)(al 121
21 n
aaa sss n→→→ − .
The set of traces (ordinary or observable) for
the behavior [B] of an MSC B can be very
huge, but it is well represented by the MSC
itself. So for the user representation it is not
necessary to come from MSC to its traces.
CTG generates traces by sequential activating
of basic protocols, so it obtains first the set of
so called BP traces, that is a sequences
n
BBB sss n →→→ −121 ...21
where 121 ,...,, −nBBB are instantiated basic
protocols, and nsss ,...,, 21 are intermediate
states. According to the semantics of concrete
implementation the resulting set of traces is
the set of traces of the system
]][*...*][*][[ 1211 −nBBBs where * means the
partially sequential composition of interpreted
MSCs. We can take for observation partially
sequential composition ][*...*][*][ 121 −nBBB
of uninterpreted MSCs, that can be well rep-
resented by vertical composition
]*...**[ 121 −nBBB of MSCs, but it may con-
tain more observable traces than needed. In-
deed, two conditional actions can be permuta-
ble as uninterpreted actions because they have
no common instances, but they are not per-
mutable because they have common attrib-
utes. To avoid the necessity of considering all
observable traces CTG assumes the following
correctness condition for MSCs: if two condi-
tion actions are not permutable as interpreted
actions, they must have at least one common
instances.
As a consequence, the CTG looks
through basic protocols entirely, but not ac-
tions and checks the permutability of basic
protocols using this easy criteria – no com-
mon instances. If two protocols are not per-
mutable, CTG consider both cases in their or-
der, otherwise only one order will be consid-
ered.
So the CTG generates the tree of BP
traces and after performance of the next basic
protocol it checks the filters. If one of the fil-
ters triggered the generating of the current
BP-trace is interrupted, this trace is written if
it is necessary to the set of generated traces,
and CTG returns to the nearest choice point to
continue the generation of the next trace.
Output. The set of generated BP-
traces with the explanations of reasons of
terminating. Each trace is contained in the
separate verdict file. CTG also produces sta-
tistic of the generation process.
Static requirements checking
Static requirement checking (SRC) tools al-
low to solve verification problems without
generating traces and exploring the state
space. For this purpose SRC uses deductive
system. The system is based on the universal
prover for the first order predicate calculi with
equality extended by some special provers
and solvers. Universal prover is based on
Glushkov evidence algorithm [11], insertion
representation of this algorithm is presented
in [2]. The specialized part of deductive sys-
tem supports proving and solving linear nu-
merical constraints for integers (Presburger
algorithm) and for reals (Furiet-Motskin algo-
rithm), proving and solving formulas for
enumerated and symbolic data types. So the
environment description for SRC is much
richer than for CTG. Especially the use of
axioms and rewriting rules are allowed. Of
course the use of arbitrary axiomatic or equa-
tional theories can lead to insolvability or in-
efficiency, so some preliminary adjustment
may be needed. Another requirement for us-
age of special theories is the possibility of
separation of subformulas belonging to differ-
ent theories if there are no procedures for their
combination.
The input of deductive system is a
closed formula (no free variables) of basic
language with all needed axioms and reduc-
tions which can be invoked preliminarily. De-
ductive system gives one of four possible an-
swers: proved, not proved, refuted and un-
known. If the statement is proved, the proof
can be printed by request. The answer not
Теоретичні та методологічні основи програмування
33
proved means that the statement cannot be
proved. If the statement is refuted, the refuta-
tion can be printed by request, and the answer
unknown means that the process failed for
lack of resources or for lack of knowledge (on
the combination of theories or equational
problems etc.).
The statement to be proved can con-
tain the occurrences of attributes. Such a
statement must be checked for arbitrary val-
ues of attributes. In this case all attributes are
substituted by variables which are bind by
universal quantifiers. For functional attributes
which occur with different arguments the sub-
stitution must be more complicated then in the
simple case.
The query for solving has the form
,...),(,...),(solve 2121 xxPxx . It is assumed that
the formula ,...),(,...),( 2121 xxPxx∃ has been
already proved. If the formula P has quantifi-
ers they are eliminated (only theories which
allow quantifier elimination are considered)
and then the formula P is simplified to obtain
the explicit solution ,..., 2211 txtx == . If the
explicit solution is not possible, than the sim-
plified formula is used as an implicit solution.
Generally a mixed solution can be obtained in
the form of conjunction of the explicit part
(conjunction of solved equalities) and the im-
plicit part (just a formula).
The problems that can be solved by
SRC are:
Transition consistency of precondi-
tions;
Completeness of preconditions;
Proving safety conditions.
Transition consistency. Let
)( βα >→<∀ ux and )( βα ′>′→<′′∀ ux are
two basic protocols. Their preconditions are
called to be consistent if they cannot be valid
at the same time. Formally it can be written
by the consistency formula )( αα ′∧¬′∀∀ xx
or )( αα ′∧′∃¬∃ xx (the lists x and x′ must
have no common variables otherwise use re-
naming). Consistency means determinism,
only one of two protocols can be applied at
the same time. If the consistency formula
cannot be proved or is refuted, we have inde-
terminism that can be undesirable and it must
be announced to user who can answer if the
discovered indeterminism is desired or not.
Completeness. The applicability con-
dition for a protocol )( βα >→<∀ ux is the
validity of the formula αx∃ . The set of basic
protocols is called complete if the disjunction
of all applicability conditions for them is al-
ways valid. So completeness means that in
any situation there must be at least one appli-
cable protocol.
Both properties are only partially rec-
ognizable because their violation is only nec-
essary condition for inconsistency or incom-
pleteness. Indeed, sometimes inconsistency
can be proved but the state that satisfies the
inconsistency may be unreachable. Therefore
we can set the inconsistency condition
)( αα ′∧′∃∃ xx as a goal state and prove its
reachability by means of CTG or STG.
Proving safety. Safety condition is an
invariant property for the system and in some
cases can be proved inductively. That is it
must be valid on any initial state and if it is
valid on some reachable state, then it must be
valid on the state obtained after the applica-
tion of a basic protocol. If it is difficult to
characterize the set of reachable states by
logic formula the tool consider arbitrary state
such that safety condition γ is valid and for
arbitrary basic protocol applicable to this state
applies this protocol formulates and calls de-
ductive system to prove the corresponding
statement. For the protocol )( βα >→<∀ ux
and safety condition γ the corresponding for-
mula is
)),(pt( γβαγ →∧∀x
where pt is the predicate transformer de-
scribed at the end of the fifth section.
Symbolic trace generator
All input files for symbolic trace gene-
rator (STG) are the same as for CTG. The dif-
ference is that an abstract model of a system
specified by a set of basic protocols is consi-
dered instead of a concrete one. The state of a
model has the form
],...,[ 1 nuuγ
where γ is a formula over attributes which
coincides with the attributed label of the envi-
ronment state and nuu ,...,1 are agents inserted
into environment. The deductive system is
Теоретичні та методологічні основи програмування
34
used for checking the applicability of basic
protocol and predicate transformer described
in the section 5 is used to obtain the next
state.
There are several modes of generating traces
controlled by the following properties;
1. Complete or incomplete set of agents.
Complete set of agents means that there are
no other agents except of those existing in the
initial state. Incomplete agent set allows in-
troducing and inserting new agents form the
virtual high level environment in the time of
generating traces.
2. Direct or inverse implementation. De-
fines which formula is used for checking ap-
plicability of basic protocol.
Basic protocols. Each protocol has
the following abstract syntax form in
symbolic notation:
))(&)(&)()(
)(&)()((Forall
xwxAxvxB
xFxux
>→<
→
The list of parameters is not separated to
agent and data parameters. The conjunction of
state assumptions u(x) is the same as in CTG.
As for CTG the first state assumption in u(x)
is a key agent assumption and has the form
,...)),(,( 21 zzsmτ where m is the name of a
key agent and can be one of parameters, s is
the (constant) name of an agent state, and
,..., 21 zz are parameters or constants. The for-
mula F(x) is the formula of basic language
without any restrictions. The expression v(x)
is a conjunction of agent state assumptions for
agents introduced by precondition, A(x) is the
conjunction of imperative statements, w(x) is
a postcondition formula (no restrictions).
B(x,y) is MSC representation of this basic
protocol.
The application of a protocol to the
current state of a system is performed ac-
cording to the rules (5a) in the case of direct
implementation or (5b) in the case of inverse
one with the following refinement for STG.
The state expression in key agent assumption
is matched with the states of all agents to get
the values of those parameters which occur in
the first state assumption and to decide which
of the agents can be used as a key agent in the
performance of the protocol. If a key agent
cannot be found in the set of agents inserted
into environment then in the case of complete
agent set the checking is failed and in the case
of incomplete agent set a new agent can be
generated and inserted into environment with
the state matched with key agent state as-
sumption. After making decision about a key
agent, and checking state assumptions for
other agents some of parameters obtain val-
ues. Moreover some of attributes can obtain
the values because for not key agents the uni-
fication, not matching is applied considering
the attributes having no definite value as vari-
ables. After that the parameters which ob-
tained values are deleted from the list of pa-
rameters and their values are substituted to the
protocol. Now the main applicability condi-
tion is checked:
)),()((| zxxRzz ∃→∀= γT
for direct implementation and
)),()((| zxxRzz ∃∧∃= γT
for inverse one. Here )(rγ is an environment
state formula, ),( rxR is the main part of pre-
condition with the explicit dependence on at-
tributes and ,...),( 21 rrr = is a list of attributes
occurring in formulas. These formulas are
valid for simple attributes and at this time
only this simple case is implemented in CTG.
Now the protocol must be instantiated for the
remained part of parameters. It is realized as
was described in the section 5 by solving the
problem )),()()((solve rxRrx →γ for direct
implementation or the problem
)),()()((solve rxRrx ∧γ for inverse one. STG
generates BP-protocols as CTG, Therefore the
termination of a protocol must be done just
after checking its applicability. This is per-
forming according to (6a) using the same
predicate transformer as in SRC.
Conclusions and related approaches
In this paper we have described inser-
tion modeling methodology, its foundations,
implementation and applications. Insertion
modeling was presented as a technology of
model driven distributed system design. This
means that the following development scheme
is adopted. First, requirements specifications
are defined, then an executable model is con-
structed, and at last an implementation is built
based on results of requirement and model
verification.
Теоретичні та методологічні основи програмування
35
This scheme was successfully piloted
in a number of industrial projects of
Motorola. Main domains of application are
telecommunication and telematics. The table
below gives a short statistics about piloting.
Project size is characterized by number of
pages in initial requirements documentation
and numbers of Basic Protocols in
corresponding formalized specification.
Fourth column demonstrates what part of
initial documentation was formalized. column
contains total number of defects found with
all VRS tools and methods but sixth gives
results of traces generators that could be used
in further testing. The last column presents
summary of engineering efforts required for
piloting.
In the proposed insertion modeling
approach an attributed transition system is
considered as a system model, requirement
specifications are defined as basic protocol
specifications. Process part of such specifica-
tions is presented as an MSC-diagram. For
verification of specifications algorithmic
(model checking) and deductive (proofs)
methods are used.
The proposed system development
and verification schemes are quite common
for a number of other approaches.
Traditional mathematical models for
specifications of concurrent systems usually
are based on process algebras (CSP, CCS,
Lotos, ACP, µCRL, π-calculus, etc.), tempo-
ral and dynamic logics (LPTL, LTL, CTL,
CTL*, PDL), and automata models (timed
Büchi and Muller automata, abstract state ma-
chines).
Classical process algebras (CSP [12],
CCS [13]) are very abstract. The states of
processes are terms; transitions specify trans-
formations of such terms. Further develop-
ment of these process algebras (ACP, µCRL,
π-calculus) extends classical models with
data, named channels and new process com-
positions. The theory of interaction of agents
and environments goes further in concretiza-
tion of process models. First, it distinguish
environment as a special agent and introduces
new composition (insertion function) of
agents into environment. It also introduces
data of various types and develops a special
action language to present processes in ab-
stract or concrete forms.
The main emphasis is paid to Basic
Protocol Specifications, which relate insertion
modeling with temporal logics.
Temporal logic is a formal specifica-
tion language for the description of behavioral
properties of non-terminating and interacting
(reactive) systems. Among such properties
traditionally are distinguished safety (“some-
thing bad never happens”), liveness (“some-
thing good will eventually happen”), and
various fairness properties (a property holds
infinitely often under certain conditions).
For example, Lamport’s TLA (Tem-
poral Logic of Actions) [14, 15], is oriented
on description of such properties and is based
on Pnueli’s temporal logic [16] with as-
signment, enriched signature, and module
specifications. It supports types (strings,
numbers, sets, records, tuples, functions) and
syntactic constructs (IF, CASE, LET, etc.)
taken from programming languages to ease
Table
Project
Reqs &
related
docs in
pages
Number
of BPs in
formaliza
tion
Coverag
e of
original
reqs
Defects
found
Generated
traces with
counter-
examples
Effort
in
staff-
weeks
Telecommunication 1 400 127 50 % 11 0 5.5
Telematics 1 200 70 100 % 10 3 5.6
Telecommunication 2 730 192 100 % 18 7 20
Telecommunication 3 ~1500 56 50 % 8 5 5.5
Telematics 2 323 219 60 % 38 8 3
Telematics 3 116 42 100 % 3 1 0.7
Telematics 4 ~1500 3005 100 % 129 7 22,5
Telecommunication 4 ~2000 2311 100 % 223 17 21,3
Теоретичні та методологічні основи програмування
36
maintenance of large-sized specifications. Be-
haviors are considered as sequences of states.
States themselves are assignments of values
to variables. A system satisfies a formula iff
that formula is true for all behaviors of this
system. Transition relation is presented by
formulae where the arguments are only the
old and new states. Such formulae present ac-
tions.
Many temporal logics are decidable
and corresponding decision procedures exist
for linear and branching time logics [17], pro-
positional modal logic [18], and some variants
of CTL* [19]. In such decision procedures
techniques from automata theory, semantic
tableaux, or binary decision diagrams (BDD)
[20] may be used.
Typically, a system to be verified is
modeled as a (finite) state transition graph,
and the properties are formulated in an ap-
propriate temporal logic. An efficient search
procedure is then used to determine whether
the state transition graph satisfies the
temporal formulae or not. This technique was
first developed in the 1980’s by Clarke and
Emerson [21], and by Quielle and Sifakis [22]
and extended later by Burch et.al. [23].
In the current version of VRS system
temporal formulas are presented implicitly
being realized with checking algorithms. Still,
future versions of the system are planned to
be extended with explicit presentation of such
formulas.
Among different verification tools we
distinguishes here the SCR toolset (Software
Cost Reduction) [24] and Action Language
Verifier (ALV) [25] which are rather close to
the VRS system.
The SCR toolset aims to verify the re-
quirement specifications of applied systems.
SCR is based on a user-friendly table notation
of finite state machines. There are tables for
the description of types, constants, variables.
Also initial restrictions, transitions and be-
havioral invariants of a specified system are
presented with tables. System variables are
divided into input (or monitored), output (or
controlled), and internal variables. Static
analysis permits to check the system model
for presence of non-determined transitions
and non-specified states. Dynamic (behav-
ioral) analysis is oriented on checking safety,
fault tolerance, and different temporal proper-
ties. All these properties are interpreted as a
safety property for a specific formula class.
Model checker is used to find counter-exam-
ple traces. The following verification tools are
used: TAME, specialized interface to PVS
prover, and SALSA, which is a specialized
solver. This solver is oriented at propositional
(quantifier-free) formulas with linear equali-
ties and inequalities.
The SCR toolset have much in com-
mon with VRS. Terminology is a little differ-
ent: for model description VRS uses basic
protocols and scenarios, and SCR uses tabular
notations, in VRS: environment and tabular
description, in SCR: dictionaries (of con-
stants, types, mode classes, variables); in
VRS: axioms for subject domains, in SCR:
environment assumptions dictionary. VRS
transition consistency, completeness and
safety checkers have SCR disjoints, coverage
and property checkers respectively.
In comparison with SCR the VRS
system for static checking uses more powerful
formulas, allowing linear equalities and ine-
qualities (both in the arithmetic of integers
and in the arithmetic of real numbers),
equalities for finitely enumerated types and
variables with indexes (attributes with pa-
rameters).
In the framework of SCR project, to
resolve the problems of behavioral properties
checking, groups of inter-supplementing tools
oriented both at inconsistency search and at
verification of specifications were created.
The same approach to the tools development
was exercised in the VRS project, where were
developed tools to cover such functionalities,
especially simulators (trace generators) for
searching of inconsistent traces at a level of
concrete and symbolic models, as well as
checkers that perform verification were de-
veloped.
Another similar tool is Action Lan-
guage Verifier (ALV) which is an infinite
state model checker. It uses linear arithmetic
constraints on integer variables for system
specification which is presented in Action
Language. Such specifications involve inte-
ger, Boolean and enumerated variables, pa-
rameterized integer constants and a set of
modules and actions composed with synchro-
Теоретичні та методологічні основи програмування
37
nous and asynchronous compositions. State-
charts and SCR specifications can be easily
translated to Action Language. Like VRS,
ALV uses symbolic model checking tech-
niques to verify or falsify behavioral proper-
ties of the input specifications. Current ver-
sion of ALV uses two different symbolic rep-
resentations for integer variables: polyhedral
and automata representation; for bounded in-
tegers BDD representation is used. These
techniques permit to construct rather powerful
symbolic model checker.
The VRS approach uses MSC as a
language for presenting system requirements.
Actually, an extended MSC is realized in
VRS checkers. This decision to orientation on
engineering languages is in good accordance
with other approaches to requirements verifi-
cation. Let us mention such MSC extensions
as Live Sequence Charts (LSC [26]), Trig-
gered Message Sequence Charts (TMSC
[27]), Object Message Sequence Charts
(OMSC [28]) and others.
Future VRS development is connected
with extension of BPS Language, and new
algorithms for symbolic checking and invari-
ant construction.
1. Letichevsky and D. Gilbert. A Model for
Interaction of Agents and Environments. In D.
Bert, C. Choppy, P. Moses, editors. Recent
Trends in Algebraic Development Tech-
niques. Lecture Notes in Computer, Springer,
1999, Science 1827,.
2. Letichevsky A. Algebra of behavior
transformations and its applications, in
V.B.Kudryavtsev and I.G.Rosenberg eds.
Structural theory of Automata, Semigroups,
and Universal Algebra, NATO Science Series
II. Mathematics, Physics and Chemistry –
Springer 2005. – Vol. 207, P. 241–272.
3. Baranov S., Jervis C., Kotlyarov V.,
Letichevsky A., and Weigert T. Leveraging
UML to Deliver Correct Telecom Applica-
tions. In L. Lavagno, G. Martin, and B.Selic,
editors. UML for Real: Design of Embedded
Real-Time Systems. Kluwer Academic Pub-
lishers, Amsterdam, 2003.
4. Letichevsky, J. Kapitonova, A. Letichevsky Jr.,
V. Volkov, S. Baranov, V.Kotlyarov, T.
Weigert. Basic Protocols, Message Sequence
Charts, and the Verification of Requirements
Specifications. Computer Networks. – 2005,
47. – P. 662–675.
5. J. Kapitonova, A. Letichevsky, V. Volkov, and
T. Weigert. Validation of Embedded Systems.
In R. Zurawski, editor. The Embedded Sys-
tems Handbook. CRC Press, Miami, 2005.
6. A.A.Letichevsky, J.V.Kapitonova, V.A.Volkov,
A.A.Letichevsky, jr., S.N.Baranov,
V.P.Kotlyarov, T.Weigert. System Specifica-
tion with Basic Protocols, Cybernetics and
System Analyses, 4, 2005.
7. International Telecommunications Union.
Recommendation Z.120 Annex B: Formal
semantics of Message Sequence Charts, 1998.
8. Reniers M.A. Message Sequence Chart: Syn-
tax and Semantics. Eindhoven, University of
Technology, 1998.
9. Letichevsky A.A., Kapitonova J.V., Kotlyarov
V.P., Volkov V.A., Letichevsky A.A. Jr., and
Weigert T. Semantics of Message Sequence
Charts, SDL Forum, 2005.
10. Letichevsky A.A, Kapitonova J.V., Kotlyarov
V.P., Letichevsky A.A. Jr, Volkov V.A. Seman-
tics of timed MSC language, Kibernetika and
System Analysis, 2002.
11. Degtyarev, J. Kapitonova, A. Letichevsky, A.
Lyaletsky, and M. Morokhovets. Evidence al-
gorithm and problems of representation and
processing of computer mathematical knowl-
edge. Kibernetika and System Analysis,
(6):9–17, 1999.
12. C.A.R. Hoare. Communicating Sequential
Processes. Prentice Hall, 1985.
13. R. Milner. Communication and Concurrency.
Prentice Hall, 1989.
14. L. Lamport. Introduction to TLA. SRC
Technical Note 1994-001, 1994.
15. L. Lamport. The temporal logic of actions.
ACM Transactions on Programming Lan-
guages and Systems, May 1994. – P. 872-923,
16. Pnueli. The temporal logic of programs //
Proc. of the 18th Annual Symp. on the
Foundations of Comp. Sci. – Nov. 1977. – P.
46–52,
17. E. Emerson and J. Halpern. Decision proce-
dures and expressiveness in the temporal logic
of branching time // J. of Comp. and System
Sci., 1985. – 30(1):1–24.
18. M.J. Fisher and R. E. Ladner. Propositional
modal logic of programs // Proc. 9th ACM
Ann. Symp. on Theory of Comp. – Boulder,
Col., May 1977. – P. 286–294.
19. Emerson E. Temporal and modal logic. In: J.
van Leeuwen editor: Handbook of Theoretical
Computer Science, Elsevier, (B):997–1072,
1990.
20. Bryant R. Graph-based algorithms for Boo-
lean function manipulation // IEEE Trans. on
Computers, 35 (8). – 1986. – P. 677–691.
Теоретичні та методологічні основи програмування
38
21. Clarke E. and Emerson E. Synthesis of syn-
chronization skeletons for branching time
temporal logic // The Workshop on Logic of
Programs, 128–143, Lecture Notes in Com-
puter Sci., 131. Springer Verlag, 1981.
22. J. Quielle and J. Sifakis. Specification and
verification of concurrent systems in CESAR.
In: Proc. 5th Intern. Symposium on Program-
ming , 142–158, 1981.
23. J. Burch, E. Clarke, K. McMillan, D. Dill, and
L. Hwang. Symbolic model checking: 10^20
states and beyond. Information and Computa-
tion, 98 (2): 142–170, 1992.
24. Constance Heitmeyer, Myla Archer, Ramesh
Bharadwaj and Ralph Jeffords/ Tools for con-
structing requirements specifications: The
SCR toolset at the age of ten, Computer Sys-
tems Science & Engineering, 1: 19-35, 2005.
25. T. Bultan and T. Yavuz-Kahveci. Action lan-
guage verifier. In Proc. of ASE 2001, 382–
386, November 2001.
26. David Harel, Rami Marelly. Come, Let’s
Play: Scenario-Based programming Using
LSCs and the Play-Engine. Springer 2003.
27. Sengupta and R. Cleaveland. Triggered Mes-
sage Sequence Charts. In Proceedings of
SIGSOFT 2002/FSE-10, 167–176, ACM
Press, 2002
28. Frank Buschmann, Regine Meunier Hans
Rohnert, Peter Sommerlad, and Michael Stal.
Pattern-Oriented Software Architecture-A
System of Patterns. Wiley & Sons, New York,
1996.
Date received 07.07.2008
About the authors:
Letychevsky Alexander,
PhD, member-correspondent of National
Academy of Sciences of Ukraine, Chair of
department
Kapitonova Julia,
PhD, Professor, Chair of department
Letychevskyi Oleksandr,
PhD, researcher
Kotlyarov Vsevolod,
PhD, leading technical specialist of Motorola
Nikitchenko Nikolaj,
PhD, Professor, Chair of department, faculty
of cybernetics
Volkov Vladyslav,
PhD, researcher
Thomas Weigert,
PhD, Professor of Computer Science, De-
partment of Computer
Science
Author’s affiliation:
Glushkov Institute of Cybernetics, National
Academy of Sciences of Ukraine, Glushkov
ave., N40,
phone: 38 044 5260058,
fax: 38 044 525 1558,
let@cyfra.net
phone: 38 044 5260058,
fax: 38 044 525 1558,
kap@d100.icyb.kiev.ua
phone: 38 044 5260058,
fax: 38 044 525,
lit@iss.org.ua
St.Petersburg software development center,
Sedova str., N14, St.Petersburg, Russia,
phone: 7 812 329 19,
fax: 7 812 329 19 12,
Vsevolod.Kotlyarov@motorola.com,
Shevchenko National Kiev University,
Glushkova ave., N2, building 6,
phone: 2590519,
fax: 521 33 45,
nikitchenko@unicyb.kiev.ua
Glushkov Institute of Cybernetics, National
Academy of Sciences of Ukraine, Glushkov
ave., N40,
phone: 38 044 5260058,
fax: 38 044 525,
vlad_volkov_98@yahoo.com
Missouri University of Science and Technol-
ogy, 500 West 15th
Street 325 Computer Science Bldg. Rolla,
MO 65409, USA (573) 341-4491,
weigert@mst.edu
|
| id | nasplib_isofts_kiev_ua-123456789-2599 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1727-4907 |
| language | English |
| last_indexed | 2025-12-07T15:31:39Z |
| publishDate | 2008 |
| publisher | Інститут програмних систем НАН України |
| record_format | dspace |
| spelling | Letichevsky, A.A. Kapitonova, J.V. Letichevsky Jr, A.A. Kotlyarov, V.P. Nikitchenko, N.S. Volkov, V.A. Weigert, T. 2008-12-15T13:20:45Z 2008-12-15T13:20:45Z 2008 Insertion modeling in distributed system design / A.A. Letichevsky, J.V. Kapitonova, V.P. Kotlyarov, A.A. Letichevsky Jr., N.S. Nikitchenko, V.A. Volkov, T. Weigert // Проблеми програмування. — 2008. — № 4. — С. 13-38. — Бібліогр.: 28 назв. — англ. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/2599 623/518.3/517.5 The paper describes insertion modeling methodology, its implementation and applications. Insertion modeling is a methodology of model driven distributed system design. It is based on the model of interaction of agents and environments [1-2] and use Basic Protocol Specification Language (BPSL) for the representation of requirement specifications of distributed systems [3-6]. The central notion of this language is the notion of basic protocol – a sequencing diagram with pre- and postconditions, logic formulas interpreted by environment description. Semantics of BPSL allows concrete and abstract models on different levels of abstraction. Models defined by Basic Protocol Specifications (BPS) can be used for verification of requirement specifications as well as for generation of test cases for testing products, developed on the basis of BPS. Insertion modeling is supported by the system VRS (Verification of Requirement Specifications), developed for Motorola by Kiev VRS group in cooperation with Motorola GSG Russia. The system provides static requirement checking on the base of automatic theorem proving, symbolic and deductive model checking, and generation of traces for testing with different coverage criteria. All tools have been developed on a base of formal semantics of BPSL constructed according to insertion modeling methodology. The VRS has been successfully applied to a number of industrial projects from different domains including Telecommunications, Telematics and real time applications.---------------- Стаття описує методологію інсерційного моделювання, її реалізацію та застосування. Інсерційне моделювання являє собою методологію проектування розподілених систем, що управляється моделлю. Ця методологія базується на теорії взаємодіючих агентів та середовищ [1-2] та використовує Basic Protocol Specification Language (BPSL) для представлення специфікацій вимог до розподілених систем. [3-6]. Діаграма Послідовності з пре- та постумовами (логічними формулами, що інтерпретуються відповідно до опису середовища) – Базовий Протокол є центральним поняттям цієї мови. Семантика BPSL дозволяє конкретні та абстракті моделі рівних рівнів абстрактності. Моделі визначені як Basic Protocol Specifications (BPS) можуть у подальшому бути використані як для верифікація специфікацій вимог та і для генерації тестових наборів. Інсерційне моделювання підтримується системою VRS (Verification of Requirement Specifications), створеною для компанії Моторола київською групою VRS у співробітництві із ЗАТ Моторола-Санкт-Петербург. Система дозволяє статичний аналіз вимог на основі автоматичного доведення теорем, символьної та дедуктивної перевірки моделей та породження трас для тестування із заданими критеріями покриття. Всі засоби були розроблені на базі формальної семантики BPSL, побудованої відповідно до методології інсерційного моделювання VRS була успішно застосована у великій кількості індустріальних проектів із різних галузей, включаючи телекомунікації, телематику та системи реального часу.---------------- Статья описывает методологию инсерционного моделирования, ее реализацию и применения. Инсерционное моделирование представляет собой методологию проектирования распределенных систем, управляемых[ моделью. Эта методология базируется на теории взаимодействующих агентов и сред [1-2] и использует Basic Protocol Specification Language (BPSL) для представления спецификаций требований к распределенным системам. [3-6]. Диаграма Последовательности с пред- и пост-условиями (логическими формулами, интерпретируемыми соответственно описания среды), называемая Базовый Протокол, – центральное понятие этого языка. Семантика BPSL позволяет конкретные и абстрактные модели разных уровней абстрактности. Модели заданные Basic Protocol Specifications (BPS) могут в дальнейшем быть использованы как для верификации спецификаций требований так и для генерации тестовых наборов. Инсерционное моделирование поддерживается системой VRS (Verification of Requirement Specifications), созданной для компании Моторола киевской группой VRS в сотрудничестве с ЗАО Моторола-Санкт-Петербург. Система позволяет статический анализ требований на основе автоматического доказательства теорем, символьной и дедуктивной проверки моделей и порождения трасс для тестирования с заданными критериями покрытия. Всеі средства были разработаны на базе формальной семантики BPSL, построенной соответственно методологии инсерционного моделирования. VRS была успешно применена в большом количестве индустриальных проектов из разных областей, включая телекоммуникации, телематику и системы реального времени. en Інститут програмних систем НАН України Теоретичні та методологічні основи програмування Insertion modeling in distributed system design Інсерційне моделювання в проектуванні розподілених систем Insertion modeling in distributed system design Article published earlier |
| spellingShingle | Insertion modeling in distributed system design Letichevsky, A.A. Kapitonova, J.V. Letichevsky Jr, A.A. Kotlyarov, V.P. Nikitchenko, N.S. Volkov, V.A. Weigert, T. Теоретичні та методологічні основи програмування |
| title | Insertion modeling in distributed system design |
| title_alt | Інсерційне моделювання в проектуванні розподілених систем Insertion modeling in distributed system design |
| title_full | Insertion modeling in distributed system design |
| title_fullStr | Insertion modeling in distributed system design |
| title_full_unstemmed | Insertion modeling in distributed system design |
| title_short | Insertion modeling in distributed system design |
| title_sort | insertion modeling in distributed system design |
| topic | Теоретичні та методологічні основи програмування |
| topic_facet | Теоретичні та методологічні основи програмування |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/2599 |
| work_keys_str_mv | AT letichevskyaa insertionmodelingindistributedsystemdesign AT kapitonovajv insertionmodelingindistributedsystemdesign AT letichevskyjraa insertionmodelingindistributedsystemdesign AT kotlyarovvp insertionmodelingindistributedsystemdesign AT nikitchenkons insertionmodelingindistributedsystemdesign AT volkovva insertionmodelingindistributedsystemdesign AT weigertt insertionmodelingindistributedsystemdesign AT letichevskyaa ínsercíinemodelûvannâvproektuvannírozpodílenihsistem AT kapitonovajv ínsercíinemodelûvannâvproektuvannírozpodílenihsistem AT letichevskyjraa ínsercíinemodelûvannâvproektuvannírozpodílenihsistem AT kotlyarovvp ínsercíinemodelûvannâvproektuvannírozpodílenihsistem AT nikitchenkons ínsercíinemodelûvannâvproektuvannírozpodílenihsistem AT volkovva ínsercíinemodelûvannâvproektuvannírozpodílenihsistem AT weigertt ínsercíinemodelûvannâvproektuvannírozpodílenihsistem |