180
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
случае телевизор продолжит работать. Более точно свойство обязатель-
ной реакции для процессов ИМИ телевизора можно перефразировать
так: если в прошлом какой-либо из этих процессов выполнял последо-
вательности
? 1.? 1., ? 2.? 1.? 2., ? 3.? 1., ? 4.? 1.? 2.? 3., ?
m z m z z m z m z z z
5.? 1.
m z
действий, то в будущем соответственно управляющее воздей-
ствие, переданное с помощью модальностей 1, 2, 3, 4, 5
m m m m m
,
долж-
но быть выполнено, т. е. процессы должны обязательно получить реак-
цию !
выключить
.
Свойства обязательной реакции !
выключить
на языке модальной
логики

1
(? 1.? 1.)
f m z
⊃
◊
1
(
),
выключить
ϕ

2
(? 2.? 1.? 2.)
f
m z z
⊃
◊
2
(
),
выключить
ϕ

3
(? 3.? 1.)
f m z
⊃
◊
3
(
),
выключить
ϕ

4
(? 4.? 1.? 2.? 3.?, 5.? 1.)
f
m z z z m z
⊃
◊
4
(
),
выключить
ϕ

5
(? 1.? 1.)
f m z
⊃
◊
5
(
).
выключить
ϕ
Аналогично на языке модальной логики могут быть сформулиро-
ваны свойства обязательной реакции !
продолжить
.
Для доказатель-
ства этих свойств методом редукции процессных выражений по
модальным формулам, задающим те или иные свойства проектных
процессов, создается тестирующий процесс. Реакции тестирующего
процесса представляют собой восприятия процесса, свойства которо-
го проверяются. В этом случае процесс называется тестируемым. Ес-
ли тестируемыми являются процессы
1 2
,
P P
,
то для свойства обяза-
тельной реакции !
выключить
тестирующим процессом будет процесс
:
тест
P
1
2
2
3
4
5
1
2
3
4
5
,
! 1.! 1.?
! 2.! 1.! 2?
! 3.! 1.?
! 2.! 1.! 2.?
! 5.! 1.! 2.! 3.?
,
,
,
,
,
тест тест тест тест тест тест тест
тест
тест
тест
тест
тест
P P P P P P P
P m z
P m z z
P m z
P m z z
P m z z z
выключить
выключить
выключить
выключить
выключить
Таким образом, выполнение процесса
тест
P
параллельно с процессом
1
P
или
2
P
для любого его подпроцесса, взаимно однозначно соответствую-
щего реакциям одной из модальностей, всегда завершается пустым про-
цессом, которому предшествуют реакция
!
выключить
со стороны про-
цессов
1
P
или
2
P
и реакция
?
выключить
со стороны процесса
i
тест
P
,
если его реакции допустимы. Следовательно, результатом редукции про-
цессов
1
i
тест
P P
&
и
2
i
тест
P P
&
всегда будет вывод: