ИСТИНА

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

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