Previous Page  8 / 18 Next Page
Information
Show Menu
Previous Page 8 / 18 Next Page
Page Background

В.С. Буренков, С.Р. Иванов

56

ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2017. № 1

В соответствии с предлагаемым методом после проведения абстракции ти-

пов данных осуществляется замена исходной модели

0

1

[

|

]

n

CS PG PG PG

моделью

0

1

2

3

[

|

],

abs

CS PG PG PG PG

в которой изначально графы

, 0 3,

i

PG i

 

являются графами

, 0 3,

i

PG i

 

исходной системы

.

CS

Пометим множество состояний системы переходов

abs

abs

TS TS CS

и ис-

ходной системы так, чтобы пометка полностью отражала состояние графов

, 0 2,

i

PG i

 

исходной системы

 

,

TS CS

а также состояние графов

,

2,

i

PG i

непосредственно используемое при модификации состояния графов

, 0 2.

i

PG i

 

Сделаем пояснения. В графах программ

, 2

,

i

PG i n

 

могут быть перемен-

ные

2

,

i

i n

v

Vstate

 

которые непосредственно участвуют в изменении значе-

ний переменных из

0 2

.

i

i

Vstate

 

Обозначим множество таких переменных

через

loc

V

,

2

.

loc

i

i n

V

Vstate

 

Значения таких переменных модифицируются

операциями извлечения сообщения из канала

1

,

c C

например,

//

2

message

i

i n

Vstate

 

coh_answers_chan ? message;

//

0 2

ack _ list

message.id

i

i

Vstate

 

, если

message.id

1, 2

ack_list

[message.id

] = false;

В ходе исполнения исходного запроса релевантны значения таких переменных

только одного процесса

. Введем такое множество переменных

,

loca

V

что его эле-

менты всегда находятся во взаимно-однозначном соответствии с рассмотренными

локальными переменными того из процессов, который проводит модификацию

переменных из

0 2

i

i

Vstate

 

:

loca

i

V Vstate

для некоторого

2

.

i n

 

Следовательно, в качестве пометок состояний абстрактной

abs

TS

и исход-

ной

 

TS

систем будем использовать множество

,

AP

AP Cond V

где

AP

V

0 2

.

i

loca

i

Vstate V

 

Последующая модификация графов программ

, 0 3,

i

PG i

 

осуществляется

путем синтаксических преобразований, описанных ниже.

Абстрактные преобразования элементов множеств

.

i

Act

Множество

выражений ограничим множеством

,

.

Cond Var Chan

Преобразования при-

сваиваний приведены ниже (символ

означает отсутствие действия).

1.

Оператор в исходной модели

 

,

.

v val v Var val dom v

  

2.

Оператор в абстрактной модели

0,1,2

, если

;

i

i

v val

v

Vstate

, если

2

.

i

i n

v

Vstate

 

Других операторов присваивания нет.

Преобразование выражений

( , )

( , )

v c Cond V C

осуществляется следующим

образом. Если

0,1,2

,

i

loc

i

V

Vstate V

то

v

остается неизменным, иначе

v

заме-