ИСТИНА

Задачи оптимизации, верификации и реорганизации программ являются центральными задачами системного программирования, требующими разработки эффективных методов решения на основе простых. В теории схем программ за многолетний период ее развития было создано несколько простых и адекватных математических моделей последовательных и параллельных программ, а также большой арсенал методов и алгоритмов семантического анализа и эквивалентных преобразований моделей программ. Цель проекта - разработка и совершенствование формальных методов структурного и семантического анализа в математических моделях последовательных и параллельных вычислений, а также создание эффективных алгоритмов решения задач оптимизации, верификации и реорганизации программ. К числу наиболее важных семантических свойств программ принадлежат отношения функциональной эквивалентности и включения, отношения симуляции и бисимуляции, свойства завершаемости, корректности и безопасности вычислений. Эти свойства исследуются в различных математических моделях программ и смежных с ними моделях вычислений – алгебраических моделях программ, различных типов автоматах, алгебрах взаимодействующих процессов. Мы рассчитываем, что методы анализа программ, разрабатываемые в указанных моделях вычислений, будут положены в основу перспективных программно-инструментальных систем синтеза, компиляции, верификации, оптимизации и реорганизации программ. Исследования по теме проекта планируется проводить по следующим четырем смежным направлениям: 1. Построение алгоритмов проверки отношений эквивалентности и включения в алгебраических моделях последовательных программ с рекурсивными процедурами, создание полных систем эквивалентных преобразований в этих моделях и их применение для решения задачи минимизации размера программ; 2. Разработка математических методов и эффективных алгоритмов реорганизации программ на основе алгоритмов проверки эквивалентности в алгебраических моделях программ; 3. Решение задач верификации параметризованных систем взаимодействующих процессов на основе моделей конечных автоматов реального времени; 4. Разработка методов синтеза, верификации и оптимизации в моделях телекоммуникационных компьютерных сетей. По этим направлениям в 2017 году планируется исследовать и решить следующие задачи. 1. Используя методы минимизации автоматов-преобразователей над полугруппами, предложенные участниками проекта в 2016 г., разработать алгоритм минимизации стандартных схем программ относительно логико-термальной эквивалентности; обосновать корректность разработанного алгоритма и оценить его сложность (исп. Захаров В.А., Попеско У.В.). 2. Используя метод совместных вычислений для разработки алгоритмов проверки эквивалентности простых программ, предложенный и развитый участниками проекта, разработать общий подход к построению полиномиальных по времени алгоритмов проверки эквивалентности в различных классах перегородчатых моделей программ с рекурсивными процедурами (исп. Подымов В.В.). 3. Используя метод верификации автоматов-преобразователей , предложенный участниками проекта в 2016 г., исследовать и найти решение задачи верификации автоматов-преобразователей, работающих над частично перестановочными полугруппами (трассами), свободными группами и абелевыми группами (исп. Захаров В.А.).

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

Для решения указанных задач планируется использовать ряд оригинальных методов и подходов, разработанных участниками настоящего проекта в ходе предыдущих исследований. Перечислим некоторые из них. 1. Методика распознавания эквивалентности для некоторых классов алгебраических программ без процедур, а именно, усовершенствованный метод «следов», метод совместных вычислений, - разработанные и развитые в ранних работах участников настоящего проекта (Р.И. Подловченко, В.А. Захаров, В.В. Подымов); эти методы являются оригинальными. 2. Методика построения полных систем эквивалентных преобразований для алгебраических моделей программ без процедур, разработанная в ранних работах Р.И. Подловченко. 3. Комбинированный метод, сочетающий процедуры унификации, антиунификации, и алгоритмы статического анализа программ, который используется для проверки логико-термальной эквивалентности и унификации моделей императивных программ; этот оригинальный метод был разработан в ранних работах В.А. Захарова. 4. Метод автоматической генерации инвариантов параметризованных распределенных систем, разработанный в ранних работах В.А. Захарова и И.В. Коннова. 5. Методы ускоренной модификации реляционных моделей программно-конфигурируемых сетей, используемые для верификации этого класса сетей; эти методы были разработаны в ранних работах В.А. Захарова и Е.В. Чемерицкого и использованы для повышения производительности процедур верификации программно-конфигурируемых сетей. 6. Методы разрыва циклических зависимостей между правилами коммутации пакетов в программно-конфигурируемых сетях. Эти методы были разработаны в ранних работах В.А. Захарова и Е.В. Чемерицкого и использованы для решения задач реконфигурирования сетей.

При выполнении проекта получены следующие основные результаты 1. Для алгебраических моделей программ с процедурами описаны новые случаи положительного решения проблем эквивалентности и эквивалентных преобразований. 2. Предложен новый метод оптимизации (минимизации по размеру) последовательных программ с использованием алгоритмов проверки эквивалентности. 3. Предложен новый метод проверки эквивалентности поведения конечных автоматов-преобразователей над полугруппами и с помощью этого метода разработаны полиномиальные по времени алгоритмы проверки эквивалентности последовательных реагирующих программ. 4. Предложены и обоснованы новые методы минимизации автоматов-преобразователей над группами и полугруппами, вложимыми в разрешимые группы. 5. Показано, что задача проверки логико-термальной эквивалентности для недетерминированных стандартных схем программ алгоритмически неразрешима. 6. Показано, что задачи минимизации стандартных схем программ и конечных детерминированных автоматов, работающих над полугруппой подстановок взаимно сводимы друг к другу; на основании этого выделен подкласс стандартных схем программ, для которого эффективно решается задача минимизации схем. 7. Разработан оригинальный язык спецификаций для описания поведения конечных автоматов-преобразователей и решена задача проверки выполнимости формул предложенного языка спецификаций относительно конечных автоматов-преобразователей.