Contemporary Problems of Social Work


Questions of verification IN distributed SOFTWARE systems

Автор/Author: Korablin Y.P., Shipov A. A.

Скачать/Download | Посмотреть онлайн/View online

Список литературы/References:

1. Karpov, Yu. G. Model Of Checking. Verification of parallel and distributed software systems. –

Publishing house of St. Petersburg: BHV, 2010. – 552 p.

2. Veldel S. A., Lukin M. A., Shaluto A. A., Yaminov B. R.Verification of automata-based programs.

– St. Petersburg: Nauka, 2011. – 244 p.

3. Korablin Y. P., Kulikova N. L., Chumakov E. Semantic methods of program analysis. – M.:

Publishing house of Rostov state construction University, 2008 – 85 S.

4. Korablin Y. p.. the Semantics of programming languages. – M.: Publishing house of MEI, 1992.

– 100 p.

4. ALAGIC, SUAD; ARBIB, MICHAEL A.. The Design of Well-Structured and Correct Programs. –

New York: Springer, 1979. – 292 p.

5. C. A. R. Hoare. An axiomatic basis for computer programming. – Northern Irelan: Queen’s

Univ. of Belfast, 1969. – 576-580 p.

References in Roman script:

1. Karpov Yu. G.. Model Checking. Verifikacia parallelnyh i raspredelennyh programmnyh system.

– Izd-vo BHV-Petrersburg, 2010. – 552 s.

2. Veldel S. A., Lukin M. A., Shaluto A. A., Yaminov B. R. Verifikacia avtomatnyh programm. –

SPb: Nauka, 2011. – 244 s.

3. Korablin Yu. P., Kulikova N. L., Chumakova E. V.. Semanticheskie metody analiza programm. –

M.: Izd-vo RGSU, 2008 – 85 s.

4. Korablin Yu. P.. Semantika yazukov programmirovania. – M.: Izd-vo MEI, 1992. – 100 s.

5. ALAGIC, SUAD; ARBIB, MICHAEL A.. The Design of Well-Structured and Correct Programs. –

New York: Springer, 1979. – 292 s.

6. C. A. R. Hoare. An axiomatic basis for computer programming. – Northern Irelan: Queen’s

Univ. of Belfast, 1969. – 576-580 s.

Содержание статьи/Article:

Recently in the field of verification the Model Checking [1] method or a method of checking

on models was widely adopted. The essence of a method consists in verification of the properties

of system presented in the form of temporal logic formulas of LTL or CTL. Thus, the verified

model can be set obviously by enumeration of all states and the edges connected to them, or

implicitly – by a set of the Boolean functions setting the relation of transitions and a set of

initial states. However, in verification of large information systems and distributed program

systems it is necessary to deal with the large number of conditions and computing processes for

their models. For example, within the program where 10 streams are at the same time carried

out and where each stream can run one of 5 different states, the total number of conditions

of computing process can reach 510 = 9765625, that can become absolute obstacles in a way

of verification for one or the other properties. Besides, models can contain those calculations,

which on practice and in real world conditions can not be executed.

The proposed method in this article of restriction of verifiable models aimed at reducing the

number of explicit computational sequences to that minimum number that will be enough to

complete the verification of certain properties. For example, to construct a model of a particular

aerotechnical system we need to perform the verification of steering systems mechanisms and

reverse engine systems. Obviously, to perform that task it is not necessary to check those

computational sequences which can run only during the aircraft flight. It would therefore be

logical at first a produce a restriction of excessive computational sequences for a given model,

and only then perform the verification of its properties.

In general terms, the operation of this method can be described as follows. For a given

model M of distributed software systems Buchi automaton Bm need to be build, that allows all

computational sequences that are possible in M. After, with LTL-formula φ “limiting” automaton

is constructed, which allows only those computational sequences that are running by φ. Then

synchronous automatons composition Bm⊗Bφ should be constructed, which carries all required

properties after applying the reduction function R.

Let’s consider the work of the proposed above method for the distributed program system

implemented on the basis of the «readers-writers» model. In our case the system will consist of

3 “writers” streams, which can make some recordings at shared resource, and 2 streams of the

“readers” having ability to make some readings from this resource. Let’s assume that always only

one of the “writers” can perform recordings to the shared resource at the same time, and any of

the “readers” can perform readings only while there are no record processes. Also let’s agree the

following condition: as soon as any “writer” wants to start writing process, process of reading

for all “readers” automatically stops. Let this model be set by structure of Kripke presented in

figure 1.1.

Figure 1.1. The Kripke’s structure for the “readers-writers” model.

Let’s construct the corresponding Buchi automaton on the basics of this model as it shown

in [1; 2] and then implement proposed method of restrictions of the verified models. Then we

will check the system for deadlocks possibility, the existence of such situations when the shared

resource will be permanently blocked by the work of one of the “writers”.

Let’s assume the following restriction for our system: “Always recording process” – with the

purpose of retaining only “writers” stream as only they are capable of taking away the resource

in unlimited use within the system’s conditions. Let’s represent this restriction statement in the

form of linear temporary logic formula: φ = G(W1 ⋁ W2 ⋁ W3).

Figure 1.2. The Buchi automaton Bm for “read-writers” model.

With the Σ we will designate the entrance alphabet of this automaton over a set of 2AP,

where Σ={∅, {W1}, {W2}, {W3}, {R1}, {R2}, {W1, W2}, …, {W1, W2, W3, R1, R2}}, AP={W1, W2, W3,

R1, R2}.

104 105


Figure 1.3. Buchi restriction automaton for LTL formula φ.

The synchronous composition of Bm⊗Bφ automatons, that meets the condition is presented

in figure 1.4.

Figure 1.4. The Buchi automaton Bm⊗Bφ.

The final result of the restriction of our model, after applying the reduction function R to the

composition Bm⊗Bφ, can be seen in figure 1.5.

Figure 1.5. The Buchi automaton R(Bm⊗Bφ).

Now available limited computing sequence of our model we will be checked out for the

existence of deadlocks. For this purpose we will use the following LTL formula: φ1 = GF(┐Wi) –

«Always in the future record process for any of streams will be surely complete». Lets take the

negation of this formula ┐φ1 = FG (Wi) and try to prove that in future we will surely meet at

least one “writer” who will never release the shared resource. Buchi watchdog automaton for

the formula ┐φ1 is shown in figure 1.6.

Figure 1.6. Buchi watchdog automaton for ┐φ1.

As can be seen from this figure, this automaton will go into accepting state only if there

is a transition labeled {Wi} and accepting state will always lead into itself only through the

transition marked by the same {Wi}. The composition of automaton R (Bm⊗Bφ) and B (┐φ1) is

shown in figure 1.7.

Figure 1.7. The Buchi automaton R(Bm⊗Bφ)⊗B(┐φ1).

In this composition there is a transition to the assuming state (S1, 2), that testifies the

formula ┐φ1 is workable, which means that our system can get into deadlock in case of work of

first “writer”. From (S2, 1) and (S3, 1) there are no transitions into assuming states, because,

for example, if we passed from the (S2, 1) state into (S2, 2) by transition {W 2}, according to

the control automaton in figure 2.6., we would have an opportunity to pass further only by

transitions, marked with {W 2}. However, from the (S2, 2) state there is a transition, for example,

into (S3, 2) state which has a transition marked with {W 3}, that obviously contradicts to our

watchdog automaton.

The development of a new technique was needed to reduce the number of testable

computational sequences of large, distributed software system models. As the result of the

accounting the specifics of verification problem the proposed method of restrictions of the

verified models was created, which allows to process verification of information systems by

taking into account their characteristic features. The main idea of this method is based on

fact that it allows you to significantly reduce the number of computational sequences in

model, which are either redundant for the verification of any of its properties, or where specific

106 107


property can not be objectively performed under real world conditions, thus allowing to simplify

and speed up the verification process.

Ключевые слова/Tags1: verification, Kripke model, Buchi automaton, temporal logic formula, LTL, CTL.