Высокоуровневое проектирование встраиваемых систем. Платунов А.Е - 73 стр.

UptoLike

ВУЗ: 

Университет ИТМО | Санкт-Петербург

Составители: 

Рубрика: 

Математический аппарат ОСМВ позволяет вычислить вектор
Ω
~
по заданному
вектору
Γ
~
.
Обозначим
Df ↑
сужение области определения функции f до ее
подмножества
)dom(
sD ⊆
. Тогда для ФБ с множеством входных портов
in
P
и
выходных
o
P
можно задать функцию
}{}{:
oinfb
PPF ↑→↑
σσ
, (1.35)
такую, что для любых двух поведений ФБ
21
,
σσ
: если
inin
PP ↑=↑
21
σσ
, то
. То есть, если поведения на входе ФБ совпадают, то они должны
совпадать и на выходе.
Отношение префикса
можно задать и для поведений. Поведения ФБ
1
σ
и
2
σ
связаны этим отношением, то есть
1
σ
2
σ
, если для всех портов ФБ
Pp
∈
:
)(
1
p
σ
)(
2
p
σ
. Отношение делает множество поведений ФБ частично
упорядоченным. С учетом наименьшего элемента
⊥
σ
(такого, что для любого
Pp
∈
:
)( p
⊥
σ
есть «пустой» сигнал
Vs
→/
⊥
0:
, не содержащий событий), это
множество становится полурешеткой, что позволяет применить к нему
результаты теории решеток и, в частности, топологии Скотта. Этот подход
используется в модели сигналов с тэгами для формального исследования
свойств различных моделей вычислений.
С точки зрения этого подхода, ФБ обладают следующими свойствами:
детерминизм (функциональность, (1.35)), монотонность (префикс сигналов на
входе дает префикс на выходе), непрерывность (монотонность при целых
сигналах), рецептивность (ФБ интерпретирует любой набор сигналов, не
нарушающий условие (1.34)) и строгая каузальность (событие на выходе может
быть сгенерировано строго после события на синхронном входе).
1.3.4.2 Вычисление временных характеристик ОСМВ ВсС на основе
денотативного описания
Рассмотрим способ вычисления временных характеристик ОСМВ ВсС в
рамках денотативного описания на основе свойств полного частично-
упорядоченного множества атрибутов компонентов модели и теоремы
Кнастера-Тарского о неподвижной точке. Предложенный способ учитывает
иерархичность моделей, допускает произвольные функции вычисления
атрибутов отдельных компонентов и использование обратной связи в модели.
ОСМВ предоставляет способ расчета вектора
Ω
, если известен вектор
Γ
,
позволяя, таким образом, вычислить выходные характеристики ФБ по заданным
входным. Если все инструкции интерпретируются функциональным блоком
последовательно (например, при программной реализации), то
ΤΓ=Ω
, (1.36)
72

Страницы