ИСТИНА

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

We are going to provide a comprehensive research on the following 4 principal lines. 1. Development of equivalence checking and inclusion checking algorithms for sequential programs with recursive procedures, development of complete systems of equivalent transformations for these models of computation and the application of these transformations to program minimization problem; 2. Development of mathematical techniques and efficient algorithms for program refactoring; 3. Development of model checking techniques for various models of programs; 4. Development of mathematical techniques for synthesis, verification and optimization of telecommunication and computer networks.

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

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

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