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

Dudnikova G.I., Zhukov V.P., Fuchs G. Density and total pressure behavior in the process of forced and spontaneous reconnection // J. Appl. Mech. Tech. Physics.–1999.– V.40.– N4.– P.558-562.–

Дудникова Г.И., Жуков В.П. Влияние вязкости на токовые слои, возникающие при распространении альвеновского импульса в гиперболическом магнитном поле // ПМТФ. Принята в печать.

Основные результаты за 1999 год состоят в следующем.

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

Разработана новая версия экспериментального средства 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. – V. 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. – C. 54-67.

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

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

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

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

По результатам совместных исследований, проведенных в последние годы д.ф.–м.н. В.И. Пинчуковым и профессором Чи-Ванг Шу – деканом факультета прикладной математики университета Брауна (США) готовится к публикации совместная монография "Численные методы высоких порядков для задач аэрогидродинамики".

На конкурс CRDF 1999-2001г. представлен совместный проект "Неявные схемы Рунге-Кутты и их применение в задачах аэродинамики".

US Army Research Office grant DAAG55-98-1-0401. "A novel principle for data processing from hand-held ground Penetrating radar".

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

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

Представлена новая, точная и быстрая процедура решения этого уравнения.

National Science Foundation grant DMS-9704923 "A fast numerical method for imaging small abnormalities in diffusion tomography".

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

Предложен эффективный метод восстановления коэффициента диффузии для двумерного случая, получено качественное отображение. Результаты были представлены на Международном симпозиуме по биомедицинской оптике (International Symposium on Biomedical Optics, BIOS’99) в Сан-Хозе (Калифорния) и опубликованы в Inverse Problems.

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

Завершена работа над рукописью монографии "Фортран-95. Учебник". Подготовлена гипертекстовая версия (см. рис. 19).

Рис. 19.

Bo Einarsson, Leonid Chubarov, and Yurij Shokin. Fortran 95 Tutorial. (отправлено в издательство Scientific Books, London)

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

В 1999 году в рамках проекта было разработано представление для недоопределенных моделей и недоопределенных вычислений Нариньяни в терминах системы логического программирования ECLiPSe. Были разработаны языки для спецификации нелинейных и комбинаторных задач, которые позволяют эффективно использовать недоопределенные модели в системе ECLiPSe. В результате реализована библиотека "Конечные множества", включающая в себя единый набор типов и эффективных алгоритмов для обработки неточных чисел и неточных конечных множеств. Базой для экспериментов и теоретического исследования являлась "Интервальная библиотека" для ECLiPSe и система LogiCalc, ранее разработанные ИСИ СО РАН совместно с Российским НИИ ИИ.

Совместно с Institut de recherche en informatique de Nantes при университете г. Нант (Франция) проделана исследовательская работа по применению методов интервального анализа в программировании в ограничениях. На базе библиотеки Опак ("OpAc"), разработанной французскими коллегами, были выполнены эксперименты по одновременному применению метода распространения ограничений и интервальных методов Ньютона, Гаусса-Зейделя с предобуславливанием для решения нелинейных ограничений. Эксперименты показали, что такой подход является перспективным при решении плотных нелинейных систем ограничений.

Yakhno T., Petrov E. Extensional set library for ECLiPSe // Proc. of the 3^rd Intern. Andrei Ershov Memorial Conf. "Perspectives of System Informatics", Novosibirsk, 1999. – Berlin a.o.: Springer, 2000. – P. 430–440. – (Lect. Notes Comput. Sci.; 1755).

Научно-исследовательский проект "Распространение системы обучения системному проектированию и создание соответствующих информационных центров в странах Восточной Европы и СНГ" по программе ИНКО–Коперникус.

Совместно с НГУ и ИАЭ СО РАН создан Центр Компетенции СБИС-технологии.

Пакеты САПР Alliance и Magic установлены и освоены в ряде научно-исследовательских учреждений, а также учебных заведений г. Новосибирска: НГУ, НГТУ, ИАЭ СО РАН.

Проведены консультации и семинары для специалистов СО РАН, на которых были рассмотрены пакеты Mentor Graphics, Cadence, Alliance.

Проведены два информационных семинара на тему "Современные СБИС-технологии" для специалистов НГУ, НГТУ, СибГАТИ, ИЯФ и др.

Проведен семинар для специалистов ИЯФ СО РАН о возможностях пакета Alliance.

Организован учебный курс по языку моделирования VHDL для студентов НГУ.

Спроектирован ряд СБИС кристаллов различных электронных устройств:

• телефонная ячейка;
• интерфейс транспьютера с шиной VME;
• координатограф для графопостроителя;
• интерфейс Intel 80186 с шиной PC AT;
• схема управления памятью.

В оглавление