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

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

В качестве формальных моделей рассматривались:

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

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

Совместно с профессором Р. ван дер Мейденом (Австралия) была исследована проблема верификации распределенных систем, использующих знания. Рассматривались системы, представленные автоматными моделями, спецификации которых выражаются формулами комбинированной логики знаний и линейного времени. Доказана неразрешимость проблемы проверки моделей (model-checking) в общем случае, и выделено два разрешимых фрагмента этой логики.

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

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

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

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

Разработана новая версия экспериментального средства EPV (Estelle Protocol Verifier), предназначенного для верификации коммуникационных протоколов, представленных на языке Estelle. Проведены успешные эксперименты по анализу, верификации и оптимизации нескольких версий протокола скользящего окна, кольцевого, а также протокола InRes.

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

Разработан прототип экспериментального средства моделирования выполнимых спецификаций распределенных систем, представленных на предложенном ранее языке Basic-REAL.

Непомнящий В.А. Верификация финитной итерации над структурами данных // Кибернетика и системный анализ. – 1999. – N 3. – C. 25-37.

Nepomniaschy V.A. Symbolic verification method for definite iteration over data structures // Information Processing Letters. – 1999. – Vol. 69, N 4. – P. 207-213.

Nepomniaschy V.A. Verification of definite iteration over hierarchical data structures // Proc. of the 2-nd Intern. Conf. on Fundamental Approaches to Software Engineering (FASE/ETAPS'99), Amsterdam. – Berlin a.o.: Springer, 1999. – P. 176-187. – (Lect. Notes Comput. Sci.; 1577).

Непомнящий В.А., Шилов Н.В., Бодин Е.В., Спецификация и верификация распределенных систем средствами языка Elementary-REAL // Программирование. – 1999. – N 4. – С. 54-67.

Непомнящий В.А., Алексеев А.Г., Быстров А.В., Куртов С.А., Мыльников С.П., Окунишникова Е.В., Чубарев П.А., Чурина Т.Г. Использование сетей Петри для верификации распределенных систем, представленных на языке Estelle // Известия РАН. Сер.: Теория и системы управления. – 1999. – N 5. – C. 105-116.

Вирбицкайте И.Б., Покозий Е.А. Использование техники частичных порядков для верификации временных сетей Петри // Программирование. – 1999. – N 1. – С. 28-41.

Вирбицкайте И.Б., Покозий Е.А. Метод параметрической верификации поведения временных сетей Петри // Программирование. – 1999. – N 4. – C. 16-29.

Virbitskaite I.B., Pokozy E.A. A partial order method for the verification of time Petri nets // Lect. Notes Comput. Sci. – 1999. – Vol. 1684. – P. 547-558.

Virbitskaite I.B., Pokozy E.A. Parametric behaviour analysis for time Petri nets // Lect. Notes Comput. Sci. – 1999. – Vol. 1662. – P. 134-140.

van der Meyden R., Shilov N.V. Model Checking of Knowledge and Time in Systems with Perfect Recall // Proc. of the19th Intern. Conf. on Foundations of Software Technology and Theoretical Computer Science (FST&TCS9), Chennai, India, 1999. – Berlin a.o.: Springer, 1999. – P. 432-445. – (Lect. Notes Comput. Sci.; 1738).

Ануреев И.С. Метод элиминации структур данных, основанный на системах переписывания формул // Программирование. – 1999. – N 4. – С. 5-15.

Korovina M.V., Kudinov O.V. A Logical Approach to Specifications of Hybrid Systems // Proc. of the 3^rd Intern. Andrei Ershov Memorial Conf. " Perspectives of System Informatics ", Novosibirsk, 1999. – Berlin a.o.: Springer, 2000. – P. 7-11. – (Lect. Notes Comput. Sci.; 1755).

Ustimenko A.P. Hierarchical cause-effect structures // Proc. of the 3^rd Intern. Andrei Ershov Memorial Conf. " Perspectives of System Informatics ", Novosibirsk, 1999. – Berlin a.o.: Springer, 2000. – P. 136-142. – (Lect. Notes Comput. Sci.; 1755).

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

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

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

Проведено исследование класса хордальных графов, для которых многие NP-полные задачи, например раскраска, имеют полиномиальную сложность, подготовлен обзор и разработан локальный алгоритм для проверки хордальности графа в модели систем переписывания графов с приоритетом. Прототипом данного алгоритма послужил алгоритм Maximum cardinality search, построенный Тарьяном и Яннакакисом. Алгоритм базируется на понятии центрального процессора, а также на разработанной новой технике "расщепляющегося заряда", которая позволяет центральному процессору осуществлять более простой и дешевый контроль за изменениями меток отдаленных вершин. Доказано, что построенный алгоритм одновременно решает задачу нахождения дерева кратчайших расстояний от центрального процессора до всех остальных вершин графа.

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

Проведено исследование методов визуальной обработки иерархических графов и графовых моделей. В рамках системы HIGRES разработаны и реализованы эффективные алгоритмы визуализации иерархических графовых моделей. Создана рабочая версия системы HIGRES.

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

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

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

Евстигнеев В.А., Касьянов В.Н. Сводимые графы и граф-модели в программировании. – Новосибирск: Изд-во ИДМИ, 1999. – 288 c.

Kasyanov V.N., Lisitsyn I.A. Support tools for hierarchical information visualization // Human-Computer Iteraction: Communication, Cooperation and Application Design. – London: Lawrence Erlbaum Associates Publ., 1999. – Vol 2. – P. 117-121.

Касьянов В.Н. Иерархические графы и графовые модели: вопросы визуальной обработки // Проблемы систем информатики и программирования. – Новосибирск, 1999. – С. 7-32.

Лисицын И.А. Применение системы HIGRES для визуальной обработки иерархических графовых моделей // Проблемы систем информатики и программирования. – Новосибирск, 1999. – С. 64-77.

Евстигнеев В.А. Хордальные графы и их свойства // Проблемы систем информатики и программирования. – Новосибирск, 1999. – С. 33-63.

Евстигнеев В.А., Бояршинов В.А. Распознавание хордальных графов в рамках распределенной модели вычислений // Проблемы систем информатики и программирования. – Новосибирск, 1999. – С. 107-129.

Бояршинов В.А. Распознавание интервального порядка на базе локальных вычислений // Проблемы систем информатики и программирования. – Новосибирск, 1999. – С.130-145.

Дылыков Ж.Л.–Д., Мурзин Ф.А., Разумов В.И., Сизиков В.П. Аксиоматика и численная интерпретация качественных моделей // Проблемы систем информатики и программирования, Новосибирск, 1999. – С. 183-187.

Мурзин Ф.А. Конструкция Париса-Кирби и проблемы сложности алгоритмов // Проблемы систем информатики и программирования. – Новосибирск, 1999. – С. 156-162.

N гос. регистрации 01.99.0010376.
Научные руководители: д.ф.–м.н. А.Г.Марчук, д.ф.–м.н., профессор В.Н.Касьянов, к.ф.–м.н. Л.В.Городняя.

Проект "Методическое и технологическое обеспечение обучения информатике и программированию".

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

В этом году при Новосибирской областной администрации сформирована рабочая группа (Предметное Жюри по информатике) по подготовке олимпиадных заданий для школьных олимпиад по информатике.

Важным достижением является включение в эту группу представителей ведущих в этом направлении организаций под руководством представителя ИСИ СО РАН им. А.П.Ершова.

Это знаменует переход к систематической работе по углубленному освоению информатики школьниками и их педагогами. На базе ВКИ и ФПК НГУ сотрудниками ИСИ СО РАН разработаны курсы по решению сложных задач и по изучению дополнительных разделов информатики, полезных при решении конкурсных задач по информатике и программированию.

Предметное Жюри осуществило подготовительную работу по подготовке заданий для районной и городской олимпиад школьников, а также по программе "Молодые информатики Сибири" (ВКИ НГУ).

Организованы занятия по методам решения олимпиадных задач со школьными учителями и школьниками Советского района, Новосибирска и Бердска.

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

Очень ярким свидетельством успехов в олимпиадном движении является победа команды НГУ на полуфинале чемпионата, проводимого АСМ.

Не так давно на этих чемпионатах новосибирские команды уступали Томску, Омску, Красноярску, Барнаулу и другим городам. В этом году уровень всех трех команд НГУ был достаточно высок, а лучшая команда заняла первое место по Сибири и четвертое по России, т.е. вошла в число шести команд, направляемых на финал. Подготовка участников команд осуществлена преимущественно сотрудниками ИСИ СО РАН, основной объем работы выполнен сотрудницей лаборатории теоретического программирования Т.Г. Чуриной.

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

Естественным продолжением этого семинара было проведение секции "Школьная информатика" на Международной конференции "Перспективы систем информатики", в рамках которой на дискуссии "Какой будет информатика в третьем тысячелетии" собран подробный и достаточно полный обзор подходов и актуальных проблем. На основе анализа этих проблем разработан проект системы непрерывной переподготовки педагогов-информатиков в рамках повышения квалификации.

Продолжается разработка научно-методических материалов образовательного и научно-популярного характера.

Завершен первый этап работы над учебно-методическим пособием "Элементарная информатика: кое-что из информатики для не очень взрослых детей".

Разработаны и опробованы разные курсы для школьников:

• "Элементарная логика" в 3-5 классах;
• "Алгоритмы и программы с элементами методов программирования" – для школьников 9-х классов;
• "Логическая алгоритмизация" – для школьников 7-х классов;
• "Программирование для физико-математического 10-го класса";
• обучение младших школьников элементам параллельного программирования.

Осуществлена проработка вводных разделов задачника по информатике для учащихся средней школы.

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

Развернута работа с младшими школьниками в КЮТе и разработка перспективного плана "Программно-методическая поддержка работы с дошкольниками и учащимися младших классов".

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

Осуществлен начальный этап по разработке информационной системы "Парадигмы".

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

В сводном издании словаря-справочника впервые собраны наиболее употребительные термины по теории графов, использованные в таких известных монографиях, как книги Ф.Харари, К.Бержа, О.Оре, А.А.Зыкова и др., а также в доступных для отечественного читателя публикациях по информатике и программированию с указанием источника и вариантов. Русский термин сопровождается его английским эквивалентом, что позволит использовать книгу как русско-английский словарь, а прилагаемый англо-русский словарь поможет при чтении англоязычной литературы. Последнее, на наш взгляд, позволит сократить размножение вариантов используемых в литературе терминов. Кроме собственно теоретико-графовых терминов в книгу включены необходимые для понимания термины из программирования, комбинаторного анализа, прикладной алгебры и исследования операций, что расширяет круг пользователей словаря.

При отборе терминов в качестве основного было выбрано множество понятий, представленных в известной монографии "Лекции по теории графов", как наиболее полного и доступного для отечественного читателя издания. Затем оно пополнялось терминами из переводных и других отечественных книг по теории графов, а также монографий по информатике и программированию, существенно использующих методы теории графов. Чтобы как-то уменьшить разрыв между терминологией монографий и терминологией, используемой в статьях и не успевшей попасть в монографии, в словарь включены термины, встречающиеся в докладах на ежегодной конференции "Graph Theory Concepts in Computer Science" и в статьях, опубликованных в ведущих по данной тематике журналах "Discrete Mathematics", "Journal of Graph Theory" и др.

Подготовлена начальная электронная версия толкового словаря, ориентированная на работу в среде Интернет и соответствующая первой редакции словаря.

Евстигнеев В.А., Касьянов В.Н. Толковый словарь по теории графов в информатике и программировании. – Новосибирск: Наука, 1999. – 288 c.

Касьянов В.Н., Евстигнеев В.А., Казанцев В.Е., Гибадуллин А.З. Толковый словарь по теории графов и его Web-версия // Новые информационные технологии в университетском образовании. – Новосибирск: ИДМИ, 1999. – С. 41-43.

Выполнен второй этап проекта создания гипертекстовой информационной системы поддержки гуманитарных исследований СИМИКС (SIMICS).

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

Проводился отбор и систематизация материала, связанного со становлением информатики в Новосибирском научном центре. В настоящее время в систему введена часть "Очерков по истории кибернетики", так или иначе связанная с деятельностью А.А.Ляпунова, информационные сообщения о работе Комиссии по системному программированию ККВТ АН СССР, обзорные статьи Н.Н.Миренкова, основополагающая статья А.П.Ершова и М.Р.Шура-Буры, а также программы курсов по программированию в НГУ.

Начаты работы по подготовке хроники событий, связанных со становлением и развитием информатике в ННЦ, и по созданию базы данных по сибирским информатикам.

Касьянов В. Н., Несговорова Г. П. Вопросы информационной поддержки гуманитарных исследований в области культуры // Проблемы систем информатики и программирования. – Новосибирск, 1999. – С. 188-201.

Касьянов В.Н., Евстигнеев В.А., Несговорова Г.П., Цикоза С.Г. СИМИКС – информационная система по истории информатики // Материалы X Междунар. конф. "Применение новых технологий в образовании". – Троицк: Фонд новых технологий в образовании "Байтик", 1999. – С. 251-252.

Разработан вводный курс программирования на Паскале в заданиях и упражнениях. Курс базируется на опыте преподавания программирования на мехмате НГУ и предназначен для использования преподавателями и студентами вузов на семинарских занятиях в ходе начального обучения программированию на языке Паскаль.

Курс содержит более 3000 задач, около четверти которых – это индивидуальные упражнения, а остальные представлены в форме заданий, каждое из которых содержит свой вариант (индивидуальную задачу) для каждого студента учебной группы. Основные приемы и методы программирования в курсе изучаются по ходу рассмотрения языка Паскаль и с использованием системы Турбо Паскаль.

В основу курса положен принцип концентрического изложения материала, когда обучаемый осваивает языковые средства и приемы программирования постепенно, слой за слоем. При этом с первых занятий студенты начинают упражняться в составлении программ, которые могут реально выполняться на доступных ЭВМ, а освоение студентом нового слоя означает просто расширение круга задач, которые он может решать. Также постепенно одновременно с расширением класса задач студенты углубляют свои знания о языке Паскаль. К концу вводной части курса они овладевают основными конструкциями языка, образующими то естественно выделяемое его ядро для "начального обучения", которое условно можно назвать языком мини-Паскаль.

В основе курса, помимо рассмотренных, лежат следующие методические и технологические принципы.

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

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

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

Касьянов В.Н. Вводный курс программирования на Паскале в заданиях и упражнениях. – Новосибирск: НГУ, 1999. – Ч. 1. – 160 c.

Касьянов В.Н. Вводный курс программирования на Паскале в заданиях и упражнениях. – Новосибирск: НГУ, 1999. – Ч. 2. – 170 c.

Касьянов В.Н. О базовом университетском образовании математиков по информатике и программированию // Материалы Междунар. конф. "Выпускник НГУ и научно-технический прогресс" – Новосибирск: НГУ, 1999. – Ч. 1. – С. 107-108.

Касьянов В.Н. Вводный курс программирования на Паскале в заданиях и упражнениях // Материалы X Междунар. конф. "Применение новых технологий в образовании". – Троицк: Фонд новых технологий в образовании "Байтик", 1999. – С. 249-251.

Касьянов В.Н. Вводный курс программирования на Паскале в заданиях и упражнениях // Материалы V Междунар. научно-методич. конф. "Новые информационные технологии в университетском образовании". – Новосибирск: ИДМИ, 1999. – С. 96-97.

Далее