автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Алгоритмический анализ поведения распределенных программ

МОСКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ вмени М.В.ЛОМОНОСОВА

Факультет вычислительной »ятематшш а кибернетики

На правах рукописи УДК 519.68

БАКАЛОВ Юрий Валерьевич

АЛГОРИТМИЧЕСКИЙ АНАЛИЗ ПОВЕДЕНИЯ РАСПРЕДЕЛЕННЫХ ПРОГРАММ

Специальность 05.13. И - математическое и программное обеспечение »ычнслителышх мзшнн, комплексов, систем и сетей

Автореферат диссертации на соискание ученой стелет! кандидата фнзико-мзтематическнх иаух

Москва 1995

МОСКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ имени М.В.ЛОМОНОСОВА

Факультет вычислительной математики и кибернетики

На правах рукописи УДК 519.68

БАКАЛОВ Юрий Валерьевич

АЛГОРИТМИЧЕСКИЙ АНАЛИЗ ПОВЕДЕНИЯ РАСПРЕДЕЛЕННЫХ ПРОГРАММ

Специальность 05.13.11 - математическое и программное обеспечение вычислительных машин, комплексов, систем и сетей

Автореферат диссертации па соискание ученой степени кандидата физико-математических наук

Москва 1996

I

Работа выполнена на кафедре автоматизации систем вычислительных комплексов факультета вычислительной атематики и кибернетики Московского государственного университета им. М.В.Ломоносова

Научный руководитель:

доктор физико-математических наук, профессор Р.Л.Смелянский

Официальные оппоненты:

доктор физико-мматематических наук. А.Я. Диковский кандидат физико-математических наук A.C. Косачев Ведущая организация

Вычислительный центр академии наук России Защита состоится ■¿Г tu>u#JL 1996 года в {!_ часов на заседании Специализированного совета д.053.05.38 К 4 по математике при МГУ им. М.В.Ломоносова по адресу: 119899, ГСП, Москва В-234, Воробьевы горы, МГУ, факультет вычислительной математики и кибернетики, аудитория 685.

С диссертацией можно ознакомиться в библиотеке факультета вычислительной математики и кибернетики МГУ.

Автореферат разослан

Ученый секретарь Специализированного совета МГУ Д.053.05.38 по математике, профессор

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

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

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

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

3

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

Основные пели работы.

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

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

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

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

Научная новизна.

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

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

Работа выполенна на кафедре автоматизации систем вычислительных комплексов, в Лаборатории вычислительных комплексов в рамках прокта по созданию интегрированной среды разработки и анализа распределенного программного обеспечения DYANA и поддержана грантом РФФИ п 95-01-01590а. Реализованная подсистема спецификаций содержит транслятор с языка спецификаций в специальное представление, позволяющее автоматически выполнять верификацию, а также программные модули, осуществляющие проверку выполнимости спецификации и ее истинность для конкретной реализации распределенной программы на языке реализации системы DYANA. Язык спецификаций имеет синтаксис, сходный с языком реализации и не требует от реализатора никаких дополнительных знаний в области математики. Система DYANA с реализованной подсистемой алгоритмического анализа демонстрировалась на международной выставке CeBIT в Ганновере (Германия) в 1995 и 1996 годах. Внедрение работы планируется продолжить в 1996 году.

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

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

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

£

опубликованы две работы, полно отражающие основные научные результаты диссертации. Прикладные результаты представлены также в ряде научных отчетов по НИР, ведущимся в Лаборатории вычислительных комплексов ВМК МГУ.

Структура и объем диссертационной работы. Диссертация состоит из введения, пяти глав, заключения, списка литературы (включающего 66 названий) и занимает 141 машинописную страницу.

СОДЕРЖАНИЕ РАБОТЫ

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

• проверка того факта, что спецификация являетей непротиворечивой;

• проверка того факта, что реализуемая распределенная программа удовлетворяет спецификации.

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

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

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

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

• безопасность (пункт 2.2 диссертации).

• гарантированность (пункт 2.3)

• обязательность (пункт 2.4)

• отклик (пункт 2.5)

• постоянство (пункт 2.6)

реагирование (пункт 2.7)

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

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

В пункте 3.8 приведены два алгоритма: алгоритм проверки истинности формулы на языке темпоральной логики вычислительных деревьев на графе переходов состояний программы и алгоритм проверки выполнимости формулы темпоральной логики линейного времени. Наличие этих алгоритмов дает возможность использования темпоральной логики в качестве формализма, используемого в системе спецификаций для автоматического решения тех двух задач, о которых говорится во введении.

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

В пункте 3.1 выделяются следующие требования к языку спецификаций:

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

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

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

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

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

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

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

• Объектно-оринтированная система спецификаций, предложенная Араписом.

• Темпоральная логика действий Лэмпорта.

• Интервальная темпоральная логика.

• Язык спецификаций DisCo.

• Система спецификаций Unity.

• Система спецификаций Munity.

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

Диаграммы Джексона. Таблицы принятия решений. Язык Estelle.

• Язык LOTOS.

• Язык SDL.

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

В главе 4 приводится неформальное описания разработанного языка спецификаций. Описание дано в виде постепенно детализируемой спецификации примера распределенной системы, описанного в пункте 2.1. В пункте 4.2, дается описание схемы функционирования распределенной системы, принятое в среде DYANA, а в пункте 5.3 обсуждается возможное отображение объектов распределенной программы из примера на такие объекты распределенной системы, как процессы, распределенные программы, - буфера и сообщения. Там же -приводятся прототипы программных процессов, использующихся для реализации примера, а также структура связей между ними. В пункте 4.4 приводятся основные понятия, используемые при спецификации: описание, ограничение, состояние, действие, вычисление, выражение поведения, свойство. Пункт 4.5 посвящен описанию общей схемы спецификации. В нем описано, из каких компонентов состоит спецификация, и далее, путем постепенного конструирования спецификации примера, вводятся все конструкции языка спецификаций. Глава завершается текстом полной спецификации примера.

В главе 5 приводятся формальные описания, семантики языка спецификаций и доказательство их эквивалентности. Во введении к этой главе (пункт 5.1) объясняется, в каком случае для описания семантики используется темпоральная логика линейного времени, а в каком -темпоральная логика ветвящегося времени. -

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

ю

В пункте 5.3 дано формальное описание синтаксиса выражения поведения - специального выражения для записи спецификации - в виде формул Бэкуса-Наура.

В пункте 5.4 дано описание семантики языка спецификаций, предназначенное для пользователя.

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

В заключении приведены основные результаты работы:

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

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

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

Публикация по теме диссертационной работы:

l.R.L.Smeliansky, Yu.P.Kazakov, Yu.V.Bakalov, The combined approach to the distributed Computer system Simulation, in Proc. Conference on Parallel Computing Technologies, Novosibirsk, Scientific Centre, Sept. 1991.

Ii

2. Ю.В.Бакалов, Р.Л.Смелянский. Язык спецификации поведения распределенных программ/ / Программирование N6, 1996 г.

3. Bakalov Yu.V., Smelianski R.L., A Language for Specifying Distributed Program Behavior//ParcelIa'96: proceedings of the VII. International Workshop on Parallel Processing by Cellular Automata and Array, Berlin, September 16 20, 1996. Akademie Verlag, Berlin.

¿JL