ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012 179
m
3,
m
5 —
только в зоне
z
1 (
расположена перед телевизором);
m
2 —
в
зонах
z
1
и
z
2
(
включает в себя пространство слева и справа от телеви-
зора);
m
4
—
в зонах
z
1,
z
2
и
z
3 (
находится сзади телевизора). Символ
с черточкой наверху, например 1
z
,
будет обозначать любой символ,
кроме
z
1.
Первый процесс:
1 11 12 13 14 15
11
12
13
14
15
,
? 1.(? 1. ? 1. ) ? 1. ,
? 2.(? 1.(? 2. ? 2. ) ? 1. ) ? 2. ,
? 3.(? 1. ? 1. ) ? 3. ,
? 4.(? 1.(? 2.(? 3. ? 3. ) ? 2. ) ? 1. ) ? 4. ,
? 5.(? 1. ? 1. ) ? 5. ,
!
.0,
!
P P P P P P
P m z G z D m D
P m z z G z D z D m D
P m z G z D m D
P
z z z G z D z D z D m D
P m z G z D m D
G выключить
D
m
.0.
продолжить
Второй процесс:
2 1 2
1
2
1
2
3
1
2
3
15
,
? 1.! .0 ? 2.! .0 ? 3.! .0 ? 4.! .0 ? 5.! .0,
? .
? .
? . ,
? 1. ? 1. ,
? 1.(? 2. ? 2. ) ? 1. ,
? 1.(? 2.(? 3. ? 3. ) ? 2. ) ? 1. ,
? 1. ? 1. ,
!
.0,
!
.0.
P S S
S m a m b m a m c m a
S aM bM cM
M z G z D
M z z G z D z D
M z z z G z D z D z D
P z G z D
G выключить
D продолжить
&
Два процесса должны выполнять идентичные функции, но опи-
сание их будет различным. Первый процесс не имеет параллельно
выполняющихся подпроцессов, а второй — содержит такую пару
подпроцессов
1 2
,
.
S S
Проверка свойств процессов.
Проверка, или доказательство
свойств проектных процессов, может осуществляться с помощью раз-
личных процедур. Одной из таких процедур является редукция про-
цессных выражений по определенным правилам [13]. Рассмотрим ее
суть на примере процессов ИМИ телевизора. Для этих процессов свой-
ства обязательной реакции с точки зрения пользователя формулируются
просто: если пользователь выполнил управляющее воздействие с по-
мощью некоторой модальности в зоне, в которой модальность может
быть распознана, то телевизор должен быть выключен. В противном