ГОСТ Р ИСО/МЭК 15414—2017
Приложение С
(справочное)
Функциональная семантика для формализованного описания поведения предприятия
Настоящее приложение представляет возможный вариант функциональной семантики для формализован
ного описания предприятия, включая свойства нормативных маркеров, формализующих обязательства, разреше
ния и запреты. Существует иной способ моделирования этих нормативных понятий. Этот подход использует идею
модели Крипке (Кпрке. реляционная или фреймовая семантика), отражающую связную совокупность (сеть) воз
можных миров и на этой основе позволяющая определить необходимые ограничения на способ возможного разви
тия системы.
С.1 Семантика для основного поведения
Во многих языках для формализации поведения, например бейсик ЛОТОС, установлена семантика, описы
ваемая в терминах маркированных систем перехода. Маркированная система перехода определена в терминах
четырех элементов:
a) совокупность государств S:
b
) совокупность действий А;
c) совокупность отношений перехода Тас S S. одно соотношение для каждого а сА;
d) начальное состояние SQсS.
Члены сообщества А.основываясь на интуиции, формулируют поименнодействия (совокупность букв исим
волов в фиксированном порядке)для определения системы. Значения элементов языка спецификации могут быть
локализованы путем формализации: для каждого элемента языка, описывающего некоторое допустимое поведе
ние. или выполнениеодного из возможныхдвйствий задается егопоследующее поведение. Повторное применение
действующих правил позволяет установить дерево следов действий, которые допускаются при фрагментации
спецификации.
Данный подход определяет непосредственно, соответствует ли наблюдаемая последовательность
действий в спецификации, и отслеживает, находится ли это поведение в пределах дерева следов. Подход широко
использовалсядля анализа того, корректно ли вычислительное поведение, ичтоболееважно, подход востребован
при анализе типовобязательств. Проблема состоит в том. чтоони (обязательства)должны быть аннулированы при
необходимости, но это может быть результатом других факторов: обязательства могут быть отложены или
отсрочены.
С.2 Структуры (фреймы) и маркировки
Модель Krlpke реализует более общий походдля выражения свойств совокупности приемлемых поведений.
Основные компоненты модели.
a) совокупность сообществ W. описанных в терминах произвольного множества логических переменных:
b
) отношение достижимости R на совокупности членов W. которое является бинарным отношением, указы
вающим. может лиодносообществобытьполученоиздругого(т. е. преобразоваться в иную совокупность):
c) отношение соответствия между членами W и паттерны намеченного поведения.
Поведенческие формулы могут включать в себя операторы, указывающие на то. что определенные виды
поведения обязательны. Это указывает, что для всех сообществ, доступных для данного сообщества, поведение
проявится в конечном счете (после произвольного числа шагов). Типы поведения, наблюдаемые в некоторых
доступныхсообществах, называются разрешенными. Таким образом, имеет местоэквивалентностьмеждуповеде
нием. которое разрешено, и тем, которое необязательно не произойдет.
Средства логических преобразований могут интерпретировать модальные операторы, проверяя на соот
ветствие условиям для совокупности доступныхсообществ. Собственно, наличие совокупности сообществ делает
такие модели эффективным инструментом по сравнению с простыми переходными сетями.
С.З вычисление полезности допустимых планов действий
Движение к модели возможныхсообществ расширяет способностьсистемы кформализации, но не разреша
ет главное противоречие при моделировании предприятия — это разрешение проблемы несоответствий. Дости
жение соответствия, рассмотренное ранее, приводит кдвойному результату, но нет указаний на то. как приблизить
цель, которая не может быть полностью достигнута.
45