Теория:

• модель функционирования многопроцессорных вычислительных систем;
• методы описания совместного поведения аппаратных и программных средств;
• методы и алгоритмы решения многопараметрических задач синтеза архитектур и планирования вычислений;
• методы спецификации и верификации свойств программ.

Программные системы:

• среда анализа и проектирования распределенных вычислительных систем ДИАНА;
• инструментальные средства синтеза архитектур ВС и планирования вычислений;
• инструментальные средства спецификации и верификации свойств программ.

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

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

2. Среда моделирования.  На основе формальной модели разработана и реализована среда моделирования ДИАНА, позволяющая:

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

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

• генетические алгоритмы;
• методы комбинирования эвристик;
• алгоритмы, основанные на пошаговом сокращении аппаратных ресурсов;
• "жадные" алгоритмы.

4. Спецификация и верификация параллельных программ.  Методы спецификации и верификации поведения параллельных программ основаны на применении модальных логик.  Моделью поведения является конечная система переходов (размеченный граф переходов).  В качестве спецификации выступает формула темпоральной логики.  Основное внимание уделяется снижению сложности алгоритмов верификации и уменьшению размера графа переходов.

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

• Моделирование и разработка программно-аппаратных специализированных и проблемно-ориентированных многопроцессорных комплексов ( в том числе и реального времени).
• Априорное, статическое и динамическое планирование параллельных вычислений.
• Отладка параллельных программ.