Исследования по теме выполнялись в рамках четырех проектов.

В рамках данного проекта для системы ЭКЛИПС (ECLⁱPS^e) разработаны Интервальная библиотека 2.0 и библиотека "Конечные множества".

Интервальная библиотека предназначена для решения нелинейных уравнений и неравенств, записанных на обычном математическом языке посредством переменных, констант, арифметических операций, прямых и обратных тригонометрических функций, функций ln, exp, max, min. Эта библиотека вычисляет для каждой переменной, задействованной в таких уравнениях, интервал, содержащий все ее возможные значения.

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

Система ECLⁱPS^e вместе с Интервальной библиотекой является удобным средством для решения задач, в которых нелинейные зависимости сочетаются с комбинаторными аспектами, — задач проектирования, финансового планирования и т.п.

Была также создана первая версия библиотеки "Конечные множества". Основной целью создания библиотеки является повышение уровня языка спецификации множеств в системе ECLⁱPS^e. Конечное множество является распространенным объектом в задачах комбинаторной природы (планирование, проектирование). Поддержка на уровне языка средств спецификации и обработки множеств существенно ускоряет создание приложений для решения таких задач.

Библиотека "Конечные множества" предназначена для решения в системе ECLⁱPS^e теоретико-множественных соотношений, связывающих переменные, константы и конечные экстенсиональные множества. Переменные могут обозначать как неизвестные конечные множества, так и неизвестные целые числа. Для вычислений с целыми числами используется Интервальная библиотека.

Для библиотеки "Конечные множества" разработан оригинальный приближенный алгоритм решения проблемы, известный как "унификация экстенсиональных множеств". Этот алгоритм дает хорошие приближенные результаты унификации (в ряде случаев—точные) и в отличие от NP-полного точного алгоритма является эффективным.

N гос. регистрации 01960002068.
Научный руководитель – к.ф.-м.н. В.А.Непомнящий.

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

В рамках метода проверки моделей (model-checking) предложен алгоритм верификации поведенческих свойств моделей распределенных систем, функционирующих в режиме реального времени.

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

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

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

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

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

Продолжалась разработка экспериментального средства ESPV (Estelle / SDL Protocol Verifier) верификации коммуникационных протоколов, представленных на стандартных языках выполнимых спецификаций Estelle и SDL. Проведены успешные эксперименты по анализу и верификации некоторых коммуникационных протоколов, представленных на языке спецификаций Estelle. В рамках этого проекта разработан метод перевода SDL спецификаций в аскрашенные сети Петри. Этот метод иллюстрируется на рис. 10 и 11, где представлены SDL спецификация блока Station_Ini известного протокола INRES, состоящего из процессов Initiator и Coder_Ini, а также соответствующая этому блоку сеть Петри. Отметим, что

Рис. 10. Описание блока Station_Ini протокола INRES

Рис. 11. Сеть для блока Station_Ini

каналу ISAP в сети соответствует два места (isap1 – входное, isap2 – выходное) для перехода, моделирующего процесс Initiator, и аналогично, каналам IPDU и MSAP в сети соответствует по два места, причем соединение переходов и мест осуществляется дугами, направление которых совпадет с направлением передачи сообщений. Начальная разметка этих мест пуста, а фишки в них могут появиться в процессе функционирования полностью построенной сети Петри, моделирующей протокол INRES.

Продолжалась разработка экспериментального средства СПЕКТР-2 верификации Паскаль/С программ. В рамках этого проекта разработан метод автоматического доказательства, основанный на системах переписывания формул, которые обобщают известные формализмы – системы переписывания термов и сужение. Исследованы свойства корректности и нетеровости систем переписывания формул. На базе этого метода реализован прототип блока автоматического доказательства и проведены успешные эксперементы.

Непомнящий В.А., Алексеев Г.И., Быстров А.В., Куртов С.А., Мыльников С.П., Окунишникова Е.В., Чубарев П.А., Чурина Т.Г. Верификация Estelle-спецификаций распределенных систем посредством раскрашенных сетей Петри.- Новосибирск, - 1998. –140с.

Тарасюк И.В. Понятия эквивалентностей для разработки параллельных систем с использованием сетей Петри // Программирование. – 1998. – N 4.

Anureev I.S. A method for simplification procedures design based on formula rewriting system // Joint Bulletin of IIS andComputer Center, Ser. Computer Science. – 1998. – N 8.

Nepomniaschy V.A., Alekseev G.I., Bystrov A.V., Churina T.G., Mylnikov S.P., Okunishnikova E.V. EPV – Petri net based Estelle protocol verifier // Proc. 1-st Intern. Workshop on the Formal Description Technique Estelle. – France, 1998. – P.101–109.

Pokozy E.A. Towards behaviour analysis of parametric time Petri nets // Ibid. – P.512–519.

Ustimenko A.P. Coloured cause-effect structures // Information Processing Letters. – 1998. – Vol.68. - N 5.

Virbitskaite I.B., Pokozy E.A. A partial order algorithm for verifying time Petri nets // Proc. International Workshop on Discrete Event Systems (WODES'98), 1998, Cagliari, Italy. – London: The IEE Publisher. –1998. – P.514–517.

Выполнен цикл работ по исследованию методов конструирования и оптимизации параллельных программ и разработке экспериментальных систем в рамках проекта ПРОГРЕСС.

Получены следующие результаты.

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

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

Выполнены исследования методов и систем оптимизирующей трансляции и конструирования программ для параллельных ЭВМ. Подготовлен обзор структур векторизующих и распараллеливающих компиляторов (CFT, CFT 2, KAP/205, Fortran-77VP, Fortran 77/SX, FORT 77/HAP, Convex, IBM 3090VF, Pascal-XT фирмы Siemens, Parafrase-2 и др.) и инструментальных систем, ориентированных на автоматическое распараллеливание программ (PAT, SUIF, Faust, FALCON, PTOPP, PEPP).

Исследовались вопросы эффективного распараллеливания методов, известных под общим названием PIC-методы, или "частицы в ячейках" (Particles In Cells) и широко применяемых в вычислительной математике при моделировании различных процессов.

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

Рассмотрен также вопрос о распараллеливании трехмерного варианта PIC-метода применительно к задаче о взаимодействии потоков разреженной плазмы в самосогласованных электромагнитных полях. Проведен также ряд исследований по распараллеливанию метода дискретных вихрей. Показано, что данные задачи поддаются эффективному распараллеливанию.

Продолжалась реализация экспериментальных подсистем (ТРАНС-ФОРМ, СФП, HIGRES и др.) в рамках проекта ПРОГРЕСС, поддерживающих хранение информации о преобразованиях, трансляцию, анализ, визуализацию и преобразование императивных и функциональных программ. Разрабатываемая система ПРОГРЕСС ориентирована на поддержку быстрого прототипирования компиляторов (в том числе оптимизирующих) для целевых архитектур и конкретных машин (VLIW- и суперскалярные, мультипроцессоры с распределенной памятью и т.д), а также поддержку исследований вопросов эффективности применения при трансляции различных систем преобразований для разных классов программ и ЭВМ, в том числе влияния на эффективность системы преобразований форм промежуточного представления программ, наборов трансформаций, их контекстных условий и стратегий применения преобразований.

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

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

Работы по теме НИР и проекту РФФИ "Понимание программ для их конструирования" (N 97-01-00724) сильно пересекаются по направлению исследований, поэтому результаты по этим исследованиям будут изложены совместно.

Была разработана модель оценки добротности информационных потоков и алгоритм проверки этого критерия добротности программ, реализована начальная версия процессора проверки такого критерия добротности, как структурная неизбыточность.

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

Исследована проблема использования потокового статического анализатора для сбора необходимой (и возможной) для целей автоматической генерации тестов информации. Создана система сбора такой информации на базе анализатора OSA.

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

Реализован или модифицирован ряд систем, связанных с этим направлением исследований.

Подготовлена к эксплуатации система параллельного программирования СуперПаскаль, создана новая версия системы, включающая контроль конфликтов параллелизма.

Подготовлен набор файлов в формате HTML, описывающий возможности разработанной гипертекстовой среды.

В рамках международного проекта открытого софтвера (система GNU) произведена языковая локализация пакета орфографического контроля Ispell и shell-интерпретатора Bash.

Подготовлено к изданию пособие по изучению стандарта языка Модула-2.

Катков С.И., Поттосин И.В. Система параллельного программирования, основанная на языке СуперПаскаль // Труды 6-го Международного семинара "Распределенная обработка информации". – Новосибирск. –1998. – С.127–131.

Кауфман А.В., Черноножкин С.К. Критерии тестированности и система оценки полноты набора тестов // Программирование. – 1998. – N 6. – С.44-59.

Куксенко С.В., Шелехов В.И. Статический анализатор семантических ошибок периода исполнения // Программирование. – 1998. – N 6. –С. 27-40.

Поттосин И.В. Добротность программ и информационных потоков // Открытые системы. – 1998. – N 6.

Уваров Д.Л. Оптимальный алгоритм чистки регулярных гамаков // Программирование. – –1998. – N 2. – С.68–80.

RescueWare Workbench представляет собой интегрированную среду реинжиниринга, учитывающую все аспекты исходной системы. Прежде всего, для каждой программы производится глубокий анализ, включая ее взаимодействия с другими программами. RescueWare снабжена мощным набором средств визуальной декомпозиции исходной программы и потому может восприниматься и как средство reverse engineering’а. Но основной акцент делается не на этом.

В RescueWare процесс реижиниринга воспринимается как решение трех основных задач. Во-первых, это перенос данных из старых баз данных и "плоских" файлов в современные реляционные СУБД. Во-вторых, производится генерация современных GUI-интерфейсов на основе старых алфавитно-цифровых экранных форм. Наконец, в-третьих, производится конвертация самих программ с учетом описанных выше изменений.

В RescueWare есть также специальная интегрированная часть, помогающая решить проблему 2000 года.

В 1998 г. были разработаны следующие инструменты:

• GlobalBRE - программа, позволяющая на основе диалога с пользователем разбить "монолитную" программу на компоненты с учетом как структурных, так и информационных зависимостей.
• DataMap - средство для формирования экранных форм на основе описания структур данных.
• LegacyDictionary - средство для так называемой рационализации имен, позволяющее корректным образом переименовывать объекты в разнородной программной системе.
• Callie - компонента, позволяющая визуализацию графа вызовов/переходов коболовских программ.
• HyperTrace - программа для "абстракной" трассировки КОБОЛ программ, позволяющая начать "выполнение" с произвольной точки программы, выбрать одну из ветвей условного оператора и в случае его достижения произвольно перемещаться как по трассе, так и по стеку вызовов, и т.д.
• HC2WWW - программа, позволяющая переносить специализированные базы данных HyperCode в HTML-файлы, которые могут быть визуализированы с помощью стандартных HTML-броузеров.

Продолжены работы по реорганизации системы HyperCode с целью обеспечения ее расширяемости и независимости от представления исходных данных. Начаты работы по созданию специализатора для КОБОЛ–программ.

Бульонков М.А., Кочетов Д.В. Визуализация свойств программ. –Новосибирск, 1998. – 38 с. – (Препр./РАН Сиб.отд-ние. ИСИ. N 51).

Продолжались работы по эффективной реализации анализатора семантических свойств, реализующего анализ отношений равенства программных термов. Основные усилия были направлены на поиск и реализацию алгоритма анализа синонимов, который бы позволил на предварительной стадии работы анализатора эффективно отыскивать нетривиальную верхнюю аппроксимацию множеств синонимов. Реализованный ранее алгоритм анализа синонимов Дейча, хотя и является достаточно "выразительным", в то же время слишком сложен для использования в качестве предварительного анализа. Среди обнаруженных алгоритмов наибольшее внимание привлек недавно предложенный алгоритм Стинсгаарда. Основанный на быстром алгоритме ОБЪЕДИНИТЬ/НАЙТИ, он позволяет за почти линейное время строить нетривиальную верхнюю аппроксимацию множеств синонимов. Также продолжались работы по сопряжению анализатора свойств с системой HyperCode.

Emelianov P.G. Analysis of equality relations: proofs and examples // Submitted to Joint NCC & IIS Bulletin, Ser. Computer science. – 1998. – N 8.

Продолжались исследования широко известной комбинаторной задачи, известной в англоязычной литературе как "Snake-in-the-Box Problem". Задача заключается в отыскании длины и эффективного конструирования максимального цикла без хорд в n-мерном единичном кубе. На данный момент известны лишь первые 5 точных значений длин. Разработана HTML-страница, содержащая обзор эквивалентных постановок задачи, известных оценок и библиографию из 58 работ. Получена новая верхняя оценка длины змеи. Составлена программа, работающая в системах UNIX/Windows 95/NT, позволяющая строить длинные змеи в кубах малых размерностей. Вычислены новые рекордные змеи для кубов размерностей 8 и 9: S₈=90 и S₉=164 соответственно.