Технология логического моделирования и анализа сложных систем
Аннотация
Предлагаются методологические, языковые и инструментальные средства для быстрого получения логических моделей систем и процессов. Язык определяется в исчислении предикатов первого порядка с равенством и допускает представление отрицаний, модулей, интервалов дискретного времени. Заданная вычислимая математическая семантика языка позволяет строить интерпретаторы, сложность которых составляет O(nlogn) относительно мощности моделей. Результат интерпретации – модель, построенная по логической спецификации объектов с помощью прямого вывода. Модель может быть использована как действующий прототип системы. Технология предназначена для решения широкого спектра задач анализа языков, проектов, процессов, разработки экспертных и обучающих систем.
Ключевые слова: логическая модель, исчисление предикатов, логические ошибки, интерпретатор, логическая семантика, анализ.
В последние годы с развитием наукоемких технологий становятся все более востребованными средства логического моделирования, позволяющие на ранних этапах проектирования систем увидеть возможные ошибки и оценить затраты ресурсов [1]. Особый интерес вызывает возможность быстрого получения логического прототипа моделируемого объекта – его статической или динамической структуры, демонстрирующей все логически связанные элементы и взаимодействия. Инструменты логического моделирования предоставляют математически обоснованные средства автоматического анализа состоятельности проектных, конструкторских, программных решений при изготовлении сложных системо-технических комплексов, анализа последствий предпринимаемых действий и аварийных ситуаций, если модель используется, например, для обучения персонала. В работе предлагаются языковые, инструментальные средства, методология логического моделирования, поддерживающие решение широкого класса задач, таких как:
- проектирование: логическое представление и анализ предметной области, быстрое создание действующих прототипов с целью раннего обнаружения ошибок проекта и оценки затрат ресурсов;
- автоматизация создания, модификация, сопровождение различных программных систем, в том числе семантических анализаторов и компиляторов;
- преобразования (декомпозиции, анализа, синтеза и модификаций) программ: внутреннее представление графов управления и зависимостей данных, обеспечение семантической корректности трансформаций программ;
- обработка данных и генерация гетерогенных систем в распределенной среде: логический анализ и проверка непротиворечивости представления различных форматов данных и запрашиваемых свойств;
- многомерная объектно-ориентированная структуризация: проверка осуществимости интеграции требуемой конфигурации из имеющейся базовой;
- анализ данных в аналитических базах данных, поддержка процедур data mining;
- обучения, создания обучающих и экспертных систем: логическое представление баз знаний, языков запросов, возможность гибкой адаптации к изменениям в предметной области.
Предлагаемую технологию составляют следующие компоненты.
Методология. Выполняются два этапа. На первом этапе составляется описание исследуемого объекта в предлагаемом логическом языке. В описание включаются: перечень сортов (доменов); элементов; их атрибутов (функций); отношений (предикатов) между ними; аксиомы, индуктивно определяющие эти отношения и атрибуты (зависимости между элементами) и аксиомы, задающие ограничения на зависимости – условия «правильности» функционирования, аварийные ситуации; параметрические схемы для представления модулей. В целом, описание должно полностью определять требуемые свойства объекта и/или его поведение. Если необходима поддержка корректности трансформаций исследуемой системы, то аналогичным образом могут быть описаны и трансформационные преобразования. На втором этапе подключаются интерпретаторы спецификаций, цель которых – построение логической модели (прототипа) объекта и диагностика выполнимости требуемых свойств. В процессе интерпретации проверяются также логические ошибки - противоречивость и неполнота представления объекта или проекта системы.
Язык логического моделирования. Для описания моделируемого объекта используется язык в исчислении предикатов первого порядка; основное отличие от Пролога и его аналогов – возможность использования модулей, отрицаний, равенства, ограниченных кванторов и переменных сорта «время» в предложениях. Основу описания - спецификации S = (,T) исследуемой системы составляют сигнатура и теория T=TDTR - множество аксиом в языке , определяющих систему (TD) и ограничивающих ее состояние или поведение (TR).Формально, = (R, F, C), где R - множество имен предикатов (отношений), F - функций (атрибутов) и C – констант; С не пусто и все константы различны. Отношение равенства считается встроенным (аксиомы равенства автоматически добавляются к TD). Константы кодируют элементы системы (например, конструкции программ или технические узлы, устройства, модули и т.п.).
Аксиомы TD рассматриваются как индуктивные определения объявленных в функций и отношений формулами вида 
или 
, где 
- вектор переменных, 
- конъюнкция атомарных формул вида 
, 
или их отрицаний (
, 
- термы сигнатуры ); 
- конъюнкция атомарных формул вида 
(определение отношения 
) или 
(определение функции 
); 
- конечный список. При каждом отношении с отрицанием 
, содержащемся в
, должен присутствовать конъюнкт 
, позитивно входящий в эту же формулу, играющий роль ограниченного квантора для 
. Подкласс аксиом TD образуют формулы без переменных: 
, составляющие множество фактов T0 - конкретных утверждений об объекте.
Ограничения ТR задаются произвольными формулами первого порядка с ограниченными кванторами.
Для спецификаций определено понятие корректности, включающее в себя свойства полноты определения функций, непротиворечивости относительно аксиом равенства и непротиворечивости относительно использования отрицаний.
Семантика языка допускает не только эффективную реализуемость, но и точную диагностику логических ошибок. Определены логическая, денотационная и операционная семантики указанного класса спецификаций и доказана их эквивалентность. В качестве логической семантики используются инициальные (минимальные относительно гомоморфного вложения) индуктивно-вычислимые (ИВ) модели из констант, обладающие свойством единственности в категории конечнопорожденных моделей и обеспечивающие возможность однозначного задания функций. Такая модель строится по спецификации, т.е. функции и отношения определяются в процессе прямого логического вывода. Доказаны [2, 3] теоремы, взаимно однозначно связывающие корректность спецификации с фактом существования модели этого типа для теории T. Построение модели не требует ограничений рекурсии в определениях и введения какого-либо упорядочивания или иерархии на множестве аксиом в T.
Интерпретаторы Операционную семантику представляют интерпретаторы, осуществляющие прямой логический вывод из TD и проверку истинности спецификаций ТR на моделях предметной области. Формально, интерпретатор вычисляет интерпретирующую функцию i ИВ-модели M=(C,i) в соответствии с денотационными уравнениями, задающими отображение сигнатурных символов на множество функций и отношений на С [3]. Для обеспечения точности диагностики логических ошибок в качестве областей данных, на которых строится функция i, рассматриваются полные решетки с низом - "неопределенность" (⊥), верхом - "ошибка переопределения" (⊤) и отношением аппроксимации ⊑: для любого элемента x области X имеет место: ⊥⊑x, x ⊑x, x ⊑⊤. Монотонность обеспечивает единственность построения неподвижной точки вычислений – результата интерпретации. Доказано, что интерпретатор строит модель M, если она существует, не зацикливается и завершает работу за конечное число шагов. Емкостная сложность интерпретации имеет порядок О(n), где n - мощность модели. Выделены условия, при которых временная сложность не превышает О(nlogn).
Поддержка модульности. Концепция и средства модульной логической спецификации основаны на идеях и методе параметризации и элементарной определимости моделей, изложенных в [4]. Пусть 0 =(R0,F0,C0) - некоторая базовая сигнатура, S0=(0,T0) – спецификация, M0=(C0,i0) - ИВ-модель спецификации S0. Применяя используемый класс спецификаций в качестве порождающего механизма для получения ИВ-моделей, можно задать иерархию моделей, используя на первом шаге i0 как начальный вход для интерпретации рекурсивных определений некоторой спецификации S1, затем полученную модель M1 как базовую для следующей итерации (S2,M2) и т.д. Поскольку модели определяются вычислимыми спецификациями, процедура построения «модели моделей» конструктивна и позволяет обосновать процесс последовательного уточнения модулей. В качестве модуля может выступать параметрическое определение отношения или функции, а также параметрическая спецификация (схема), используемая, например, как генератор типов. Соответственно параметром может быть модель (множество исходных фактов), множество констант, спецификация (определение конкретного отношения или функции), параметрическая спецификация (модуль).
Представление динамических свойств. Допускается включение переменных времени в логические формулы. Переменные пробегают конечные интервалы H дискретного набора точек, каждая из которых может задаваться либо конкретной датой, либо событием (именем или сигналом события). Например, интерпретация предложения: t0, tH (сигнал(t0) tt0 режим(t)) установит состояние режим для временных точек интервала H после момента t0 – времени наступления события сигнал. Такого рода спецификации использовались для моделирования космических тренажеров, где время получения сигнала и входа в требуемое состояние было точно задано.
Использование переменных времени позволяет обеспечить монотонность вычислений при интерпретации трансформаций структуры объекта или преобразовании модели, а также сохранять историю проекта в рамках единой языковой и инструментальной среды.
Несмотря на сложное математическое обоснование, практические спецификации выглядят ясно и просто. Например, все правила видимости переменных в языке Модула-2 составляют четыре аксиомы-определения и две аксиомы-ограничения, описывающие контекстные условия. По этим аксиомам автоматически генерируется семантический анализатор языка – интерпретатор, строящий модель - внутреннюю структуру программы.
Часть предлагаемых средств использовалась для создания тренажеров, обучающих проведению стыковки космических объектов. Возможность динамического изменения спецификаций определила удобный способ задания аварийных ситуаций и отработки реакции при неправильной подаче или приеме сигналов, а также позволила обнаружить ошибки в проектах программ, реализующих процесс стыковки. Метод и класс спецификаций апробировались также для разработки языковых процессоров и технологии генерации сетевых приложений из объектно-ориентированной базы-заготовки.
Литература
1. Чернов, А.В. Синтез интеллектуальных самотестируемых устройств для систем управления электроэнергетическими объектами [Текст] // Известия высших учебных заведений. Электромеханика, 2009. – № 2. – С.65-68.
2. Ильичева, О.А. Инициальная семантика логических спецификаций с отрицанием [Текст] // Кибернетика и системный анализ, 1992. – №4. – С.13-19.
3. Ильичева, О.А. Средства эффективной диагностики ошибок для систем логического прототипирования [Текст] // Автоматика и телемеханика, 1997. – №9. – С.185-196.
4. Гончаров, С.С., Свириденко, Д.И. +-программы и их семантики [Текст] // Вычислительные системы, 1987. – №120. – С.24-51.