Тезисы докладов

отчетные доклады по молодежным грантам СО РАН

Молодежный проект "Спецификация и верификация комплексных систем" направлен на решение фундаментальных проблем в исследовании открытых вопросов в теориях комплексных систем. В рамках проекта проводилось исследование двух классов комплексных систем.

Первый класс составляют гибридные системы --- одна из активно развивающихся областей информатики. Круг проблем в данной области связан с моделированием, контролем, синтезом, спецификацией и верификацией таких систем. В этой области проведены следующие исследования:

1. В рамках теории областей Ершова-Скотта предложен новый подход к вычислимости на действительных чисел. На едином языке даны основные определения: вычислимости функций, операторов, функционалов.

2. На языке теории определимости дана характеризация классов вещественнозначных вычислимых функций, операторов и функционалов. Так, вычислимые вещественнозначные функции могут быть описаны двумя sigma-формулами. Истинностное значение данных формул определяет полностью вычислимую функцию. Для операторов и вещественнозначных функционалов получены аналогичные характеризационные теоремы. Исследованы свойства непрерывности, областей определения вычислимых объектов.

3. В рамках разработанных теоретических основ вычислимости на действительных числах предложен подход к спецификации гибридных систем на языке теории областей. При данном подходе непрерывная часть гибридной системы описывается вычислимым функционалом.

Другой класс комплексных систем составляют распределенные системы реального времени (протоколы коммуникаций, системы управления производством, системы автоматического диспетчерования транспорта и т.д.). Они состоят из большого числа компонентов со сложным характером взаимодействий, что затрудняет понимание природы разнообразных процессов, протекающих в системе. Поэтому проектирование и реализация корректных распределенных систем реального времени возможны только при использовании формальных методов и средств, которые должны быть, с одной стороны, 'дружественными' для разработчиков, а с другой -- математически строгими и адекватно представлять структуру и поведение систем. В этой области проведены следующие исследования:

1. Предложена аксиоматизация для бисимуляции в алгебраической системе BPA. Получена формульная характеризация бесконечных событий в структуре событий посредством введения новой алгебры PBPA, расширяющей BPA добавлением оператора параллелизма и модификацией операции последовательной композиции. Построена семантика формул данной алгебры. Предложена частично упорядоченная характеризация алгебры процессов с итерацией.

2. Построена операционная семантика потоковых сетей посредством ACP-термов. Установление соответствия между моделями, задающими семантику потоковых сетей с помощью структур событий и следовых языков соответственно.

3. Разработан комбинированный модельный язык, включающий подъязыки выполнимых и логических спецификаций. Он ориентирован на спецификацию и верификацию распределённых систем, представленных на языке SDL. Описаны его формальный синтаксис и семантика, базирующиеся на SDL и логике ветвящегося времени CTL. Полная структурная операционная семантика выполнимых спецификаций фиксирована в виде систем переходов. Доказаны теоремы о свойствах семантики языка --- теорема о совместимости семантик уровней языка, теорема об устойчивости к заиканию, теорема об интерливинговом параллелизме и отсутствии конкурентного доступа к каналам. Описан проблемно-ориентированный подход к верификации распределённых систем. В рамках этого подхода предложен метод верификации свойств прогресса спецификаций модельного языка. Проведены эксперименты по верификации спецификаций, написанных на модельном языке.

Спецификации каждого из рассмотренных классов комплексных систем имеют свои особенности и, соответственно, свои методы верификации. Однако можно выделить общие свойства спецификаций: использование структур данных и наличие временных ограничений. В этой области проведены следующие исследования:

1. Введено новое понятие ветвящегося сужения. Ветвящееся сужение расширяет обычное сужение на разбор случаев. Предложена стратегия ветвящегося сужения, сохраняющая эквивалентность замкнутых all- и exists-формул. Стратегия формализуется в рамках систем переписывания формул. Выделены три класса конструктивных систем переписывания формул --- системы элиминации анализаторов, системы элиминации анализаторов со статусом и системы элиминации анализаторов с базой подстановок. Доказана их завершимость (нетеровость) относительно стратегии редукции "самый внутренний". Введено новое средство преобразования формул --- системы пополнения формул. Предложен критерий сохранения выполнимости формул при этом преобразовании. Приведен способ задания с помощью систем пополнения формул таких известных средств преобразования формул, как (обычные, условные и ассоциативно-коммутативные) системы переписывания термов, упрощающие замены переменных, разбор случаев, пополнение множества формул за счет следствий из аксиом.

2. Разработан метод сведения типов данных, определяемых конструкторами, к базовым математическим структурам (множествам, мультимножествам и кортежам) и частичные разрешающие алгоритмы для базовых структур, основанные на системах переписывания формул. Алгоритм проверки выполнимости формул арифметики Пресбургера распространен на ряд функций над кортежами. Показано, что расширения арифметики Пресбургера некоторыми целочисленными функциями сводимы с помощью систем переписывания формул и систем пополнения формул к обычной арифметике Пресбургера.

3. Реализован прототип доказателя, позволяющего проверять свойства на структурах данных и временные ограничения. Разработан новый язык спецификаций SIMPLE, используемый в качестве входного языка доказателя. Описан метод доказательства бескванторных формул языка SIMPLE.

Примечание. Тезисы докладов публикуются в авторской редакции

Ваши коментарии Обратная связь

[Головная страница] [Конференции]

© 1996-2001, Институт вычислительных технологий СО РАН, Новосибирск
© 1996-2001, Сибирское отделение Российской академии наук, Новосибирск