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

На правах рукописи

?Г6 ОД

• -7*0

Сараикин Андрей Витальевич

Методы анализа корректности параллельного и распределенного программного обеспечения на основе РБ-сетей

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

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

Томск —2000

Работа выполнена в Томском политехническом университете

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

доктор технических наук, профессор Н.Г. Марков

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

доктор технических наук, профессор В.П. Бондарепко кандидат технических наук В.Н. Бурлаков

Ведущая организация:

Институт систем информатики

Сибирского отделения Российской академии наук

Защита состоится Дс/декабря 2000г. в в ауд. 3.1 к на заседании диссертационного Совета Д 063.80.03 при Томском политехническом университете по адресу: 634034, г. Томск, ул. Советская, 84, институт «Кибернетический центр» ТПУ.

С диссертацией можно ознакомиться в библиотеке Томского политехнического университета по адресу: 634034, г. Томск, ул. Белинского, 55.

Автореферат разослан « /Л ноября 2000 г.

Ученый секретарь диссертационного Совета к.т.н., доцент

.Л. Чудинов

Общая характеристика работы

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

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

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

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

• наличие описательных средств, максимально удобных для практического применения при проектировании ПРПО;

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

В качестве наиболее приемлемого в этом смысле ФМП в [8, 11] предлагается и развивается аппарат PS-сетей.

Актуальность данной темы определяется необходимостью создания новых и совершенствования предложенных ранее методов анализа ПРПО, описываемых на основе PS-сетей.

Исследования и разработки по теме проводились в соответствии с утвержденными штанами ПИР института «Кибернетический центр» ТПУ, и были включены в 1995-1998 гг. в Государственную Hill «Трансферные технологии, комплексы и оборудование» (подраздел «Программные системы»).

Фундаментальные исследования по теме «Разработка моделей и методов проектирования программного обеспечешы мультипроцессорных вычислительных систем» выполнялись в 1992-1994 гг. по Гранту Миннауки России.

Прикладные исследования проводились в рамках ряда хоздоговорных и госбюджетных НИР, в том числе по НИР, включенной в Межвузовскую НТП "Геоинформационные системы" Минобразования России (Проект 04.0003.99).

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

корректности ПРПО на основе аппарата PS-сетей. Для достижения этой цели работе решаются следующие задачи:

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

2. Разработка методов и алгоритмов, позволяющих посредством выявлени поведенческих свойств PS-сетей осуществлять анализ корректности описывае мого на их основе ПРПО.

3. Создание программных средств, реализующих предложенные методы ] алгоритмы.

4. Исследование эффективности предложенных методов, алгоритмов i созданных программных средств, для чего следует решить ряд задач анализ корректности проектируемого ПРПО.

Методы исследований. В работе использованы методы теории множестЕ теории линейной алгебры, теории алгоритмов, теории графов и комбинаторию и теории моделирования.

Научную новизну полученных в работе результатов определяют:

1. Формальные определения поведенческих свойств PS-сетей и методы об наружения этих свойств, предназначенные для обоснования корректности про ектируемого ПРПО;

2. Матричное представление аппарата PS-сетей, а также теоретике множественное и матричное представления базового подкласса аппарата PS сетей — BPS-сетей, предназначенных для формального анализа поведенчески: свойств описываемого на их основе ПРПО;

3. Алгоритмы эквивалентных преобразований над PS-сетями, позволяю щие осуществлять приведение PS-сети к BPS-сети с сохранением ее поведение ских свойств;

4. Теория асинхронной интерпретации BPS-сетей, опирающаяся на ря, теорем, доказанных автором, и позволяющая на основе решения уравнения СА перехода расширить возможности анализа BPS-сети в части применения метод; инвариантов;

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

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

Практическая ценность и реализация результатов работы. Практиче ски значимыми являются созданные модели, методы, алгоритмы и программ ные средства для анализа проектируемого ПРПО на предмет его корректности Программные средства функционируют на ПЭВМ типа IBM PC в операцион ной среде Windows 95/NT. Объем разработанного на языке С++ ПО составляе-более 6500 строк программного кода.

Предложенные модели, методы и алгоритмы, а также разработанные программные средства анализа ПРПО были внедрены в Государственном научно-исследовательском институте информационных технологий и телекоммуникаций «Информика» г. Москва при проектировании и исследовании корректности способов организации распределенной обработки информации в проекте «ГИС-сервер социально-экономической сферы субъекта федерации», разработанного для использования в сети Internet. Эта же методы, алгоритмы и программные средства внедрены при исследовании верхних границ времени выполнения операций над данными пользователями «Регионального банка геологической информации по геологии нефти и газа и недропользованию», разработанного в Западно-Сибирском геологическом научно-аналитическом центре г. Тюмень. Созданные программные средства анализа ПРПО также были внедрены в учебный процесс в Томском политехническом университете. Результаты внедрений подтверждаются соответствующими актами о внедрении.

Основные положепня, выносимые на защиту:

1. Предложенные методы и алгоритмы анализа ПРПО позволяют исследовать его корректность еще на этапе проектирования.

2. Теория асинхронной интерпретации BPS-сети существенно расширяет возможности анализа поведенческих свойств описываемого на их основе ПРПО.

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

4. Разработанные теоретические положения, методы, алгоритмы и программные средства позволяют проектировать надежное и эффективное ПРПО.

Апробация работы. Основные результаты работы докладывались и обсуждались на Международной конференции «Фундаментальные и прикладные проблемы охраны окружающей среды» (г. Томск, 1995 г.), на Международной конференции «Всесибирские чтения по математике и механике» (г. Томск, 1997 г.), на I Международном симпозиуме по науке и технологии KoRus'97 (г. Ульсан, Южная Корея, 1997 г.), на П Международном симпозиуме по науке и технологии KoRus'98 (г. Томск, 1998 г.), на VI Международном семинаре «Распределенная обработка информации» РОИ'98 (г. Новосибирск, 1998 г.), на III сибирском конгрессе по прикладной и индустриальной математике ИНПРИМ'98 (г. Новосибирск, 1998 г.), на IV Международном симпозиуме по науке и технологии KoRus'2000 (г. Ульсан, Южная Корея, 2000 г.).

Публикации. По результатам исследований опубликовано 14 работ, в том числе 9 статей.

Личный вклад:

1. Постановки ряда рассмотренных в диссертации задач выполнены совместно с Н.Г. Марковым и Е.А. Мирошниченко, при этом математические формулировки задач исследований осуществлены автором.

2. Разработка и формулировка определений PS-сетей, их маркировки и

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

3. Постановка задачи исследования корректности способов организации распределенной обработки информации в ГИС-сервере социально-экономической сферы субъекта федерации осуществлена совместно с Н.Г. Марковым и П.М. Острасть, разработка моделей ГИС-сервера проведена совместно с Е.А. Мирошниченко. Результаты исследования получены автором.

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

Объем и структура работы. Диссертация состоит из введения, четырех глав, заключения, списка использованной литературы из 101 наименования и приложений. Объем основного текста диссертации составляет 123 страницы машинописного текста, иллюстрированного 35 рисунками и 9 таблицами.

Содержание работы

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

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

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

Анализируются проблемные задачи, связанные с обеспечением корректности ПРВ. Обосновывается выбор подхода, состоящего в использовании ФМП при описании и обосновании корректности как ПРВС, так и разрабатываемого для них ПРПО. На основе проведенного анализа формулируются общие требования, которым в комплексе должны удовлетворять ФМП, используемые при проектировании ПРПО.

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

Обосновывается выбор РБ-сетей как наиболее удобной ФМП для описания и анализа ПРПО на этапе его проектирования.

Формулируются цель и основные задачи, решаемые в диссертационной работе.

Во второй главе излагаются развитые автором теоретические основы ап-

парата PS-сетей, на которых базируются разработанные методы анализа их поведенческих свойств.

Дается теоретико-множественное определите аппарата PS-сетей.

PS-сеть N-{V,D, Т, R, F, Р, А, 5) характеризуется непересекающимися конечными множествами вершин V, дуг D, ресурсов R, функций использования ресурсов F= {Ar~, Ar*} (/' = 1,|£>|, j = 1,|Л|, |f]=|£)|x|/?|), назначаемых дугам,

классов предшествования Р, определяемых на парах дуг, классов альтернативы А, определяемых на парах подмножеств дуг In (множество альтернативных входов) и Out (множество альтернативных выходов), классов одновременности S, определяемых на взаимно непересекающихся подмножествах дуг и значениями длительностей активаций Т, сопоставляемых дугам. Функционирование PS-сети характеризуется ее состоянием — маркировкой Л/ в момент времени /. Множество J(M)cS всех возбужденных при маркировке М классов одновременности в PS-сети называется фронтом возбуждения. В PS-сети изменение маркировки осуществляется в результате активации дуг некоторого максимального неконфликтного подмножества классов G(M)cJ(M), называемого фронтом включения. Обозначим как G'{M) множество всех дуг, входящих в классы фронта G(M). Поведение PS-сети моделируется последовательностями фронтов включения либо вида Г2 = G'(hf)%G'(Mx),..., либо вида Qs = G{hP),G{M),..., называемых допустимыми фронтами включения. При этом множество маркировок, порождаемых допустимыми последовательностями фронтов включения, называется множеством достижимости и обозначается Л4°).

Формулируются формальные определения поведенческих свойств PS-сетей.

Определение 1. Вершина veV (ресурс reR) в маркировшшой PS-сети (N, Л*°> называется k-ограниченной (к-ограниченным), если для любой достижимой га маркировки M(V) (M(R)) найдется целое неотрицательное число к такое, что M(v) < к (А/(г) < к). Если такого к не существует, вершина v (ресурс г) неограниченная (неограниченный). Если вершина v, либо ресурс г ограниченные при к < 1, то они называются безопасными.

Определение 2. Маркированная PS-сеть {N.hf) называется ограниченной, если для каждой ее вершины ve V и каждого ее ресурса reR найдется такое число к > 0, что V и г — ¿-ограниченные. Если для какой-то ve V, либо какого-то reR такого к не найдется, то PS-сеть называется неограниченной. Если для всех ve Vii всех reR к < 1, то PS-сеть называется безопасной.

Определение 3. Класс одновременности seS в

PS-сети (N, Л/> называется квазиживым, если существует достижимая га hf маркировка М, при которой s возбужден.

Определение 4. PS-сеть (N, Л/') называется квазиживой, если все ее классы одновременности квазиживые.

Определение 5. Класс одновременности seS в PS-сети

(N, Л/°> называется живым, если из любой достижимой из маркировки существует последовательность фронтов включения, содержащая s. Т.е. любая допустимая последовательность фронтов включения может быть продолжена таким образом,

чтобы было возможным включение 5. Если это условие в РБ-сети {К Л/) не выполняется, то класс одновременности 5 называется мертвым.

Определение 6. РБ-сеть (Ы, А/0) называется живой, если все ее классы одновременности живы.

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

Формулируются формальные определения матричного представления РБ-сети. Вводятся дополнительные операции над матрицами.

Определение 7. Пусть имеется РБ-сеть Д Т, Я, /\ Р, А, 5>. Мат-

ричный вид РБ-сети N—это кортеж К:

N = <0+, 1Г, А+, А , Р\ Р , Б, Т),

где = МДяхл, т =|£>1, и = | У\ (г^=1, если d, входит в V,, иначе — <^=0);

0 = М;]«*« (^=1, если dl выходит из иначе — ¿о=0);

К" = [г,Лт,!, Гу =Аг~\

А+ =[ау]м«/,/=Ы| (аи=1, если с!,еОщ, иначе — а,у= 0);

А" = [йг0]™*/ (а,/=1, если с1, еЦ, di еа,, иначе — 0);

Р* = [р^уь, Ь =1 (/7,у= 1, еслиPi={d¡, с1к\ иначе —ри= 0);

Р = 1Рч]т*ь (р,у=1, еслиpjH.dk, 4), иначе —0);

[>,Дпхс, с=Ы (5/У=1, если d,eSj, иначе — %=0);

Т = (У//=г,, если /=7, иначе — (и= 0);

Определение 8. Маркировка М РБ-сети N в матричном виде есть четверка

М = (ту, я, у, тг),

где ту =[/иу,]1хя, тг, — число маркеров в вершине V,; ц — количе-

ство включений дуги у =[у,-] 1хт, у, — число тактов до выключения дуги тг =[/и/-,]1х/, тг, — объем ресурса /у,

Обозначим как Е, е = (1,1,...,1) единичную матрицу и единичный вектор-строку соответственно, а как g — вектор фронта включения размерности такой, что если М') и 0, в противном случае. Далее мы также бу-

дем использовать другое обозначение вектора фронта включения — где ^1=1, если и ^¡=0, в противном случае.

Характеристической суммой двух чисел а и Ь будем называть число с = тах(а,Ь), обозначаемое как с = а+Ь.

Характеристическим произведением матрицы Х/хш на матрицу Утхл будем называть матрицу Ъы„ (обозначается как 2=Х®У), где элементы определяются как +х,2Уу+ ...+х:ту^.

Операция бинарного выбора: Ъ = Xе = [г(;]/хя, если дг,/=1, и г,7=0 в противном случае.

Операции сравнения. Пусть аир — векторы-строки с целочисленными элементами, а ={аь а2,..., а/}, Р={/?1, А,..., Д}- Определим операции сравне-

ния а<(3, а^р, а = Р, а^р, а>риа>р следующим образом:

1) a < р — "true", если V/: /< / at<fi, ииаче — "false"-,

2) а < р — "true", если V;': ;< / а,<Д и 3/': 0</ «/<$, иначе — "false"-,

3) a = р — "/гае", если V/: 0£ /< / , иначе — '/a/se";

4) a * р — "true", если 3ij: OS /< /, OS j< I a,<P, и иначе — "false"-,

5) a > p — "true", если V/': 0< /< / а,>Д, иначе — "false"-,

6) a > p — "true", если V/: Ой i< I a,>fi и 3j: Ой j< I a}>ft, иначе — "false"-,

Определение 9. Назовем класс одновременности s„ в PS-сети возбужденным в маркировке М, если выполняется совокупность следующих условий:

1) во всех начальных вершинах дуг из s„ есть маркеры: mv-[S.„]r®D~>0;

2) никакая дуга из s„ не включена: y-S>,„= 0;

3) для всех дуг из sn выполнены условия предшествования:

q(P+-P>[S..„]r-r>0;

4) для всех дуг из s„ выполнены условия альтернативных включений:

e+q(A+-A-HS..„]rA>0;

5) включение дуг го s„ не уменьшит объем никакого ресурса до отрицательного значения: mr-[S. „]r-R >0.

Определение 10. Фронтом включения G(M)qJ(Щ в PS-сети называется любое максимальное подмножество фронта возбуждения 1{М) такое, что для него выполняются следующие условия:

1) суммарное потребление дугами всех классов из G{M) любого ресурса не превышает его объем: mr-g

2) во всех классах из G(M) нет двух дуг, входящих в одно и то же множество альтернативных входов: g А~<1.

Определение 11. Пусть в момент t состояние PS-сети определяется маркировкой Л/. Тогда маркировка А/+1 вычисляется на основе следующих уравне-шш, описывающих правила изменения маркировки:

1) перераспределение маркеров в вершинах: mv'+,=mv'+[y']e<g>D+-g'®D~;

2) изменение объемов ресурсов: mr,+ l=mr'+[y']s-R+-g'-R~;

3) подсчет количества включений дуг: q'+1=q'+[y']fl;

4) перераспределение маркеров по дугам: у'+1 =y'+g'-(T-E)+[e-y']s-e.

Последовательное применение этих правил позволяет формировать протокол функционирования PS-сети на интервале модельного времени [0, Щ аналогично тому, как это делается в случае теоретико-множественного представления.

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

Определение 12. Деревом покрытия для PS-сети называется

граф T(N, М°), который строится в соответствии со следующим алгоритмом.

1) корень дерева обозначается М° (компоненты mv и mr°);

2) вершина, обозначенная вектором М'-1, имеет исходящую дугу, помеченную G, и ведущую в вершину М', если для маркировки М'~' может быть

сформирован фронт включения;

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

4) компоненты вектора М' вычисляются следующим образом:

a) если на пути из вершины М° в вершину М' есть вершина М* (0<ж/) такая, что ту^ту'" 1 +[у'~1 1 и либо g'r"1*g'"l, либо g'r~l=g'"1) то

для тех V/, для которых шу,'г<шу|",+[у'"1]в ФБ^-^'"1®^,; для всех остальных V, шу|=ту5~|+[у'"1]в Аналогичным же образом

вычисляется вектор шг';

b) если на пути из вершины М° в вершину М' нет вершины М* (0 <тг< <) такой, что шу^ ту'"1 +[у'"']8 ® Б- Б" и либо g'r~1*g'",, либо е^-1^'-1, то шу'= ту'"1 + [у'"']в ® О - g'"1® Э". Аналогичным же образом вычисляется вектор тг';

5) вершина, обозначенная вектором М, не имеет исходящих дуг в следующих случаях:

a) если при М нельзя сформировать ни одного фронта включения;

b) если на пути го вершины М° в вершину М' есть вершина М* (0 <к< /) такая, что ту* = ту' и тг* = тг'.

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

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

Определение 13. Локальным тупиком называется такое подмножество Р'сР, заданных на подмножестве 5"сД которое образует направленный цикл ожидания одного класса из 5'другим.

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

Определение 14. 5Р-инвариантом РБ-сети называется целочисленный неотрицательный вектор-строка г = (г^ ..., :„), удовлетворяющий условию:

/•(8Г®Р+ - 8Г®Р~) = 0.

Каждый 5Р-инвариант РБ-сети представляет собой булев вектор, при этом, если г,= I, то класс одновременности s, eS принадлежит циклу ожидания, образующему данный локальный тупик.

Одним из этапов данного метода является этап построения порождающего множества ^-инвариантов на основе алгоритма Тудика.

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

ВРБ-сеть N-{7, Д Я, /% 5) характеризуется непересекающимися конечными множествами вершин V, дуг Д ресурсов Я, функций использования ресурсов /■■= {Аг~,АГу } (/'= 1,|С|, _/' = 1,|/?|, |/г]=Д|х|й|)5 назначаемых дугам, классов одновременности Б, определяемых на взаимно непересекающихся подмножествах дуг. Функционирование РБ-сети характеризуется ее состоянием — маркировкой А/ в момент времени (. При этом длительность активации любой дуги ВРБ-сети равна 1.

Определение 15. Четверка {V, Д Я, Л/°(Р)> ВРБ-сети называется ее структурной компонентой, а четверка (Б, Я, Л/(7?)) — ресурсной компонентой.

Определение 16. ВРБ-сеть BN в матричном представлении есть кортеж BN = Б , И", Б), где = [с1ц\тхп, т=|д1,л=1И (^=1, если с/, входит в у,, иначе —

О" = [с/,,]„,,<„ (<3/7=1, если (1, выходит из иначе — ^-0);

8 = С -1(^=1, если с1, €5,, иначе — 0);

Определение 17. Маркировка М ВРБ-сети BN в матричном виде есть двойка М = (ту, тг), где ту =[/яу,]¡х„, тг, — число маркеров в вершине V,; тг =[/иг,]] тг, — объем ресурса г,;

Определение 18. Назовем класс одновременности в ВРБ-сети возбужденным в маркировке М, если выполняется совокупность следующих условий:

1) во всех начальных вершинах дуг из .?„ есть маркеры: ту-[8.,„]г®0">0;

2) включешге дуг из не уменьшит объем никакого ресурса до отрицательного значения: тг-[8. „]ги >0.

Определение 19. Фронтом включения С(М)^(М) в ВРБ-сети называется любое максимальное подмножество фронта возбуждения 1(М) такое, что для него выполняются следующее условие: суммарное потребление дугами всех классов го С(Л/) любого ресурса не превышает его объем — тг-« ■!* >().

Определение 20. Пусть в момент I состояние ВРБ-сети определяется маркировкой А/. Тогда маркировка Л/+1 вычисляется на основе следующих уравнений, описывающих правша изменения маркировки'.

1) перераспределение маркеров в вершинах:

шу'+1= ту' + ¿®1Г (1)

2) изменение объемов ресурсов:

т^^тг' + ^^-^Я- (2)

Предложена теория асинхронной интерпретации ВРБ-сети, базирующаяся

на понятиях линейной и полулинейной определенности ВР5-сети и на уравнении синхронно-асинхронного перехода (СА-перехода). Теория предоставляет возможность анализа поведенческих свойств на основе метода инвариантов. Операция характеристического произведения «®», введенная в определении РБ-сети для реализации механизма слияния и размножения маркеров при ее синхронной интерпретации, не является линейной операцией (для нее, в частности, не выполняется аксиома об обратном элементе). Поэтому данная теория имеет целью представить ВРБ-сеть в виде, позволяющем с определенными ограничениями осуществить замену операция «®» на операцию матричного произведения «*» и тем самым перейти к асинхронной интерпретации ВРБ-сети.

Дадим некоторые из определений теории.

Обозначим как V (°у) множество дуг (множество классов одновременности), входящих в вершину V, а как V* (у°) — выходящих из вершины V.

Определение 21. Линейно определенной называется ВРБ-сеть, структурная компонента которой удовлетворяет условиям:

1) УуеГ,1М>1=» N=1;

2) УуеГ,|у|>1 => И=1.

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

Определение 22. Полулинейно определенной называется ВРБ-сеть, структурная компонента которой удовлетворяет двум условиям:

1) УУ,, у;е У( М >1)&( |°у,| >1) (У,°П°У, = 0);

2) УуеК(М£2)&(И<2).

Обозначим как Сг„с матрицу, строки которой однозначно соответствуют фронтам включения £ из множества всех возможных фронтов включения для некоторой ВРБ-сети ВЫ (порядок фронтов не существенен), а как бь^ — вектор-строку, каждый элемент которого 5, — есть целое неотрицательное число, соответствующее количеству вхождений /-го фронта ^ в О5. При этом 2с-1.

Пусть 0^2л= ||с^„®8г®в;хя I Ов7" <ЭО-хл|. Пусть также ранг матрицы © (далее будем называть ее характеристической матрицей ВРБ-сети) равен с (с <2п). Обозначим как некоторый /-й, произвольно выбрашшй базис, а через ©~х2л матрицу, состоящую ш с базисных строк матрицы ©, и ®4-гх2л— матрицу, образованную остальными ее строками. Тогда имеет место равенство

- ©1

©•Г5-0 • (3)

Учитывая, что ©* = С-0', где С — матрица преобразования размерности £ - с х с, и разложив левую часть равенства (3) на сумму, получим

(5'+5"-С)-0'=5© (4)

Наконец, обозначив в (4) выражение в скобках через 61х?, имеем

6-0' = 5© (5)

Поскольку в матрицах 0 и 0' базисными являются только с столбцов, номера которых соответствуют номерам столбцов матрицы 0' (далее будем называть ее базисной матрицей ВРБ-сети), то без потери общности в (5) они могут быть заменены матрицами и ©', где 4х — матрица, сформированная из базисных столбцов матрицы 0 (будем далее называть ее базисной характеристической матрицей). Умножив левую и правую части уравнения (5) справа на обратную к матрице 0' матрицу (©')' и, приняв В = ¥ ■(©')'> имеем

|[Е

5 = 5-В = б „ С

(6)

Уравнения (5) и (6) будем называть уравнениями синхронно-асинхронного перехода или уравнениями СА-перехода ВР8-сети.

Возможность построения уравнения СА-перехода устанавливается следующей теоремой.

Теорема 1. Для любой ВРБ-сети линейно или полулинейно определенного вида может быть построено конечное, но не пустое множество уравнений СА-перехода.

Определение 23. Базисная матрица 0' ВРБ-сети линейно или полулинейно определенного вида и, соответственно, ее уравнение СА-перехода называются правильными или, что то же самое, уравнение СА-перехода имеет решение, если матрица преобразования удовлетворяет условию С > 0.

Следующие теоремы и следствия из них устанавливают способ построения уравнения СА-перехода.

Теорема 2. Определитель характеристического произведения матриц С и в7 отличен от нуля.

Следствие. Любые с <, £ строк (столбцов) характеристического произведения матриц в и линейно независимы, следовательно, ранг характеристической матрицы ВРБ-сети равен числу с отличных друг от друга столбцов составной матрицы ЦБ7, ®В* :8Г®0~||. Соответственно, базисная матрица

ВРЗ-ссти может быть определена с любыми, линейно независимыми строками ее характеристической матрицы. На основании данного следствия можно утверждать о возможности получения правильной базисной матрицы непосредственно из матриц Б* и Б", что подтверждается следующей теоремой.

Обозначим как в^« матрицу, образованную с строками матрицы в, такими, что некоторая /'-я базисная матрица равна ©' = С'®Б, где Б — матрица размерности сх с , образованная с отличными друг от друга столбцами составной матрицы Цв7 ®Б+ ; Бг ® 0~|, а как — матрицу, образованную остальными ее строками.

Теорема 3. Пусть матрица Б получена для структурной компоненты линейно или полулинейно определенной ВРБ-сети, тогда & = С®Э есть правильная базисная матрица, если С' = Бг.

Условия данной теоремы определяют способ получения правильной ба-

зисной матрицы и как следствие — способ получения матрицы ©', а именно ©'= ¡Ог ®8Г<2Ю+ | ®БГ ®0~|. При этом уравнения (1) и (2), обобщаются

на случай произвольных последовательностей включения 6: ту' = ту0 +5-С°и тг' = тг° + 6-Ся, где С° и С" — матрицы инцидентности соответственно структурной и ресурсной компоненты линейно или полулинейно определенной ВРБ-сети при ее асинхронной интерпретации.

Определение 24. ЗКЛ-инвариантом ВРБ-сети называется целочисленный неотрицательный вектор-столбец у = (уь ..., упч)т, удовлетворяющий условию [|с° ! ся|-у=о.

5КЛ-инвариант соответствует понятию р-инварианта в теории СП, характеризующего консервативную компоненту этой сети и для которой известно, что все позиции консервативной компоненты СП ограничены при любой начальной маркировке. Положения предложенной теории позволяют утверждать, что где ЛУ°) — множество достижимости для асин-

хронно интерпретированной линейно или полулинейно определенной ВРБ-сети. Из чего можно сделать вывод о том, что если некоторая вершина или ресурс являются ограниченными при асинхронной интерпретации, то они ограниченные и при синхрошюй интерпретации. Обратное, очевидно, не верно. Таким образом, 5ГЛ-инварианты позволяют устанавливать свойство ограниченности для тех вершин и ресурсов, для которых оно может быть установлено как структурное свойство.

Определение 25. Ж-инвариантом ВРБ-сети называется целочисленный неотрицательный вектор-строка х = (Х|, ...,х„), удовлетворяющий условию:

х-Цс0 : Сй|| = 0.

Ж-инварианты соответствует понятию /-инварианта в теории СП. Они характеризуют стационарно повторяющие последовательности фронтов включения и необходимы при выявлении свойств квазиживости и живости ВРБ-сети.

Предлагается метод анализа поведенческих свойств ВРБ-сети, основанный на итерационном способе формирования порождающих множеств 5УЛ- и £0-инвариантов с использованием алгоритма Тудика.

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

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

Для решения задачи преобразования ВРБ-сети к ВРЗ-сети полулинейно определенного вида предлагаются алгоритмы ¿^///-преобразований.

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

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

Для решения задачи уточнения временных характеристик объектов у'-го уровня иерархии при интеграции объектов у-1-го уровня иерархии разработан способ масштабирования модельного времени.

Для анализа ПРПО на основе PS-сетей в рамках инструментальной системы моделирования «Parallax» созданы программные средства (рис. 1), предоставляющие пользователю следующие основные возможности: обнаружение в модели локальных тупиков; осуществление преобразований PS-сети к BPS-сети; построение дерева покрытий (достижимости) для PS- и BPS-сети; осуществление преобразований BPS-сети к BPS-сети полулинейно определенного вида; интерпретация вариантов поведения приведенной BPS-сети; построение SVR- и SD-инвариантов.

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

Решена задача моделирования на основе PS-сетей временных задержек переменной длительности для

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

Рассмотрена задача исследования корректности проектируемых способов организации распределенной обработки информации в ГИС-сервере социально-экономической сферы субъекта федерации, разработанного по заказу Государственного научно-исследовательского гшститута информационных технологий и телекоммуникаций «Информика» г. Москва. ГИС-сервер предназначен для организации удаленного доступа пользователей к функциям геоинформационной системы средствами Web-технологии и создавался как важный компонент распределенной геоинформационной системы.

При проектировании ПО для ГИС-сервера решена задача реализации в нем механизма уничтожения просроченных сеансов. Исследовался следующий механизм уничтожения сеансов. В сеансе сохраняется время последнего обращения пользователя (получения запроса). При превышении заданного предела времени ожидания (таймаута) происходит уничтожение сеанса В ходе анализа

Рис. 1 Структура программных средств анализа ПРПО

разработанных моделей ГИС-сервера (одна из моделей представлена на рис. 2), в частности, строились 5РЛ-инварианты для исходных данных с более чем 200 вершинами и 200 ресурсами, на что было затрачено менее 1 минуты (при асимптотической экспоненциальной от размерности оценке временной сложности алгоритма, лежащего в основе используемого метода). При этом проведенные исследования показали, что такой механизм удаления просроченных сеансов не надежен, поскольку допускает удаление сеансов, для которых время таймаута вышло, а обработка накопившихся запросов не окончена. Эти и другие полученные результаты послужили основой для внесения изменений в проектные решения, что в конечном итоге способствовало разработке надежного ПО ГИС-

Рассмотрена задача исследования верхних границ времени выполнения операций Select, Insert, Delete и UpDate над данными, возникшая при проектировании «Регионального банка геологической информации по геологии нефти и газа и недропользованию» (РБГИ). Используемая при этом технология «клиент-сервер» позволяет клиентам осуществлять доступ к данным банка в многопользовательском режиме. Ввиду того, что различия по времени выполнения этих операций велики, потребовались исследования влияния количества клиентов банка, выполняющих операции по изменению данных (формирователи) и количества клиентов, осуществляющих только выборку данных (пользователи) на время выполнения каждой конкретной операции. Проведенные исследования разработанных моделей банка данных позволили получить ряд таких зависимостей в вид( аналитических формул, достоверность которых обосновывается с использова нием предлагаемых в работе методов и алгоритмов анализа корректносп ПРПО.

Полученные зависимости были использованы для определения верхи и; границ времени выполнения операций над данными в РБГИ (некоторые резуль таты на рис. 3), а также для определения соотношения количества формирова телей N и пользователей М при условии, что верхняя граница времени вы пол нения операций над данными не превысит 10 секунд по К.Р. Боффу (рис. 4).

Полученные результаты позволили принять решение о необходимости вы деления в РБГИ абонентского пункта (пунктов) для увеличения количества об служиваемых одновременно пользователей РБГИ. Разработанные модели и ps

wmt tm gi.i— . ► • ti If Ь

| МММ > • йм.» ~ Ьт, Сммн • Имм WM ч на QJ ■ ■■■ -- ftw/ ¿J я« .J С 1 \ Cw».l mm J / *J \ О / » 5ю1

Рис. 2 Фрагмент РБ-сети, моделирующей ГИС-сервер при обслуживании им трех сеансов

зультаты их исследования составили также основу для разработки методологии эффективного использования РБГИ.

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

в

Рис. 3 Зависимость времени выполнения операции ЦрОа1е от количества формирователей N при фиксированных значениях количества пользователей М

Рис. 4 Диаграмма соотношений количества формирователей N и пользователей М, при котором время выполнения операции ирОа1е с учетом блокировки общей записи меньше 10 секунд

Основные результаты работы

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

1. Сформулированы формальные определешм, характеризующие поведенческие свойства РБ-сетей при исследовании корректности описываемого на их основе ПРГГО.

2. Разработаны метод анализа поведенческих свойств РБ-сетей на основе модификации алгоритма построения дерева покрытий и метод обнаружения локальных тупиков в РБ-сети, основанный на поиске ¿¡У-инвариантов.

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

4. Разработан метод анализа поведенческих свойств ВРЗ-сети, базирующийся на решении уравнения синхронно-асинхронного перехода и понятиях йУЯ- и Ж-инвариантов, введенных в рамках предложенной теории асинхронной интерпретации ВРБ-сети.

5. Разработан ряд алгоритмов преобразований над Р8- и ВРБ-сетями, позволяющие осуществлять приведение произвольной РБ-сети к ВРБ-сети полулинейно определенного вида.

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

и

разверток метадуг.

7. Созданы программные средства, реализующие предложенные методы и алгоритмы анализа корректности ПРПО, описываемого на основе PS-сетей. Разработанное ПО функционирует на ЮМ PC-совместимых ПЭВМ под управлением ОС Windows 95/NT и состоит из более чем 6500 строк программного кода на языке С++.

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

9. Разработанные методы, алгоритмы, программные средства, модели и результаты исследований моделей внедрены в Государственном научно-исследовательском институте информационных технологий и телекоммуникаций «Информика» г. Москва и в Западно-Сибирском геологическом научно-аналитическом центре г. Тюмень. Программные средства анализа ПРПО также внедрены в учебный процесс в Томском политехническом университете.

Основные публикации по теме диссертации

1. Markov N.G., Miroshnichenko Е.А., Ostrast P.M., Sarajkin A.V. Using PS-nets for Analysis of Parallel Processes Interaction in Application Server // In: Proceedings of the 4th Korea-Russia Int. Symp. on Sci. and Tech. — Ulsan, Ulsan University, 2000, part 2. — p. 75-79.

2. Markov N.G., Miroshnichenko E.A., Sarajkin A.V. Analysis of Parallel Computation Correctness With the Use of PS-nets // In: Proceedings of the 2nd Korea-Russia Int. Symp. on Sci. and Tech. — Tomsk, 1998. — p. 281-285.

3. Markov N.G., Miroshnichenko E.A., Sarajkin A.V. Analysis of Parallel Computation Correctness With the Use of PS-nets // In: Abstracts of the 2nd Korea-Russia Int. Symp. on Sci. and Tech. — Tomsk, TPU, 1998. — p. 253.

4. Markov N.G., Miroshnichenko E.A., Sarajkin A.V. Method and Tools for Parallel and Distributed Software Creation // In: Proceedings of the 1st Korea-Russia Int. Symp. on Sci. and Tech. — Ulsan, Ulsan University, 1997. — p. 389-394.

5. Markov N.G., Miroshnichenko E.A., Sarajkin A.V. Method and Tools for Parallel and Distributed Software Creation // In: Abstracts of the 1st Korea-Russia Int. Symp. on Sci. and Tech. — Ulsan, Ulsan University, 1997. — p. 205.

6. Markov N.G., Miroshnichenko E.A., Sarajkin A.V. Technology of Design of Distributed Applications with the Use of PS-nets // Join Bulletin of NCC and IIS, Series Computer Science, Novosibirsk. — №12, 1999. — p. 32-36.

7. Марков Н.Г., Мирошниченко E.A., Сарайкин A.B. PS-сети — новый аппарат моделирования параллельных процессов // В кн. Тез. докл. Междунар. конф. «Всесибирские чтения по математике и механике». — Томск, ТГУ, 1997. — Т. 1,—с. 209-210.

8. Марков Н.Г., Мирошниченко Е.А., Сарайкин А.В. PS-сети — формальный аппарат моделирования параллельных процессов И В кн. Математическое и программное обеспечение САПР. — Томск, ТПУ. — 1997. — с. 68-85.

9. Марков Н.Г., Мирошниченко Е.А., Сарайкин A.B. Метод декомпозиции для расчета полей пластовых давлений при подземном захоронении промышленных отходов и его реализация на многопроцессорных вычислительных системах // В кн. Тез. докл. Междунар. конф. «Фундаментальные и прикладные проблемы охраны окружающей среды». — Томск: изд-во 11 У, 1995. — с. 117.

10. Марков Н.Г., Мирошниченко Е.А., Сарайкин A.B. Методы и средства моделирования и анализа параллельного программного обеспечения на основе аппарата PS-сетей // В кн. Математическое и программное обеспечение САПР. — Томск, ТПУ. — 1997. — с. 86-97.

11. Марков Н.Г., Мирошниченко Е.А., Сарайкин A.B. Моделирование параллельного программного обеспечения с использованием PS-сетей // Программирование. — 1995. — № 5. — с. 24-32.

12. Марков Н.Г., Мирошниченко Е.А., Сарайкин A.B. Применение аппарата PS-сетей при проектировании распределенных приложений // В кн. Распределенная обработка информации (труды шестого Международного семинара), Новосибирск, СО РАН. — 1998. — с. 264-268.

13. Марков Н.Г., Мирошниченко Е.А., Сарайкин A.B. Технология проектирования распределенных приложений с использованием PS-сетей // В кн. Тез. докл. Третьего сибирского конгресса по прикладной и индустриальной математике (ИНПРИМ-98). Часть V. — Новосибирск: Изд-во Института математики, 1998, — с. 48.

14. Сарайкин A.B. Сравнительный анализ моделирующей мощности PS-:етей и классических сетей Петри // Кибернетика и ВУЗ. — 1999. — Вып. 29. —

83-94.

; • ; Подписано к печати 15.11.2000. Формат 60x90/16. Бумага офсетная N»1 МИФ^Вь Печать RISO. Усл.печл 1.11. Уч.-изд. 1.0. Тираж 100 экз. Заказ №207. ТПУ ИПФ ^ Лицензия ЛТ №1 от 18.07.94. Типография ТПУ.

634034, Томск, пр.Ленина, 30.

ВВЕДЕНИЕ.

ГЛАВА 1 ПРОБЛЕМЫ ОБЕСПЕЧЕНИЯ КОРРЕКТНОСТИ ПРВ.

1.1 Основные понятия, характеризующие ПРВ.

1.2 Проблемы корректности ПРВ.

1.3 Требования к формальным моделям параллелизма.

1.4 Классификация и анализ формальных моделей параллелизма.

1.4.1 Структурные модели. Сети Петри и их расширения.

1.4.2 Семантические модели.

1.4.3 Логические модели.

1.5 Цель и задачи исследования.

Одной из самых сложных и актуальных проблем технологии программирования является проблема обоснования надежности программного обеспечения (ПО), приобретающая особое значение в связи с массовым внедрением в практику параллельных и распределенных вычислительных систем (ПРВС) [71]. Поэтому при проектировании параллельного и распределенного ПО (ПРПО) к традиционным задачам разработки ПО [80] добавляется ряд более сложных задач, связанных с необходимостью правильной организации параллельных и распределенных вычислений (ПРВ) [71, 72].

Чаще всего актуальная проблема обоснования надежности ПРПО сводится к проблеме обоснования его корректности. Решение последней основывается на использовании формальных моделей параллелизма (ФМП), позволяющих анализировать поведенческие свойства ПРПО [72, 73, 92].

В настоящее время предложено и исследовано большое количество ФМП ориентированных на решение различных задач, связанных с ПРВ и отличающихся, главным образом, степенью детализации моделируемых процессов и явлений. Наиболее развитыми ФМП являются сети Петри и их расширения. Важные результаты по этим ФМП обобщены в работах Питерсона Дж., Котова В.Е. и ряда других исследователей. Однако анализ показывает [85, 89, 90], что среди предложенных ФМП нет таких, которые бы в комплексе предоставляли следующие возможности:

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

• наличие описательных средств, максимально удобных для практического применения при проектировании ПРПО;

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

В качестве наиболее приемлемого в этом смысле ФМП в [83, 86] предлагается и развивается аппарат Р8-сетей.

Актуальность данной темы определяется необходимостью создания новых и совершенствования предложенных ранее методов анализа ПРПО, описываемых на основе Р8-сетей.

Цель работы и задачи исследования. Целью диссертационной работы является создание математического и программного обеспечения для анализа корректности ПРПО на основе аппарата Р8-сетей. Для достижения этой цели в работе решаются следующие задачи:

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

2. Разработка методов и алгоритмов, позволяющих посредством выявления поведенческих свойств РБ-сетей осуществлять анализ корректности описываемого на их основе ПРПО.

3. Создание программных средств, реализующих предложенные методы и алгоритмы.

4. Исследование эффективности предложенных методов, алгоритмов и созданных программных средств, для чего следует решить ряд задач анализа корректности проектируемого ПРПО.

Апробация работы. Основные результаты работы докладывались и обсуждались на Международной конференции «Фундаментальные и прикладные проблемы охраны окружающей среды» (г. Томск, 1995 г.), на Международной конференции «Всесибирские чтения по математике и механике» (г. Томск, 1997 г.), на I Международном симпозиуме по науке и технологии КоКш'97 (г. Ульсан, Южная Корея, 1997 г.), на II Международном симпозиуме по науке и технологии КоЯш'98 (г. Томск, 1998 г.), на VI Международном семинаре 7

Распределенная обработка информации» РОИ'98 (г. Новосибирск, 1998 г.), на III сибирском конгрессе по прикладной и индустриальной математике ИНПРИМ'98 (г. Новосибирск, 1998 г.), на IV Международном симпозиуме по науке и технологии КоЯш^ООО (г. Ульсан, Южная Корея, 2000 г.).

По результатам исследований опубликовано 14 работ, в том числе 9 статей.

Личный вклад:

1. Постановки ряда рассмотренных в диссертации задач выполнены совместно с Н.Г. Марковым и Е.А. Мирошниченко, при этом математические формулировки задач исследований осуществлены автором.

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

3. Постановка задачи исследования корректности способов организации распределенной обработки информации в ГИС-сервере социально-экономической сферы субъекта федерации осуществлена совместно с Н.Г. Марковым и П.М. Острасть, разработка моделей ГИС-сервера проведена совместно с Е.А. Мирошниченко. Результаты исследования получены автором.

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

Коротко изложим основное содержание работы.

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

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

Анализируются проблемные задачи, связанные с обеспечением корректности ПРВ. Обосновывается выбор подхода, состоящего в использовании ФМП при описании и обосновании корректности как ГТРВС, так и разрабатываемого для них ПРПО. На основе проведенного анализа формулируются общие требования, которым в комплексе должны удовлетворять ФМП, используемые при проектировании ПРПО.

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

Обосновывается выбор РБ-сетей как наиболее удобной ФМП для описания и анализа ПРПО на этапе его проектирования.

Формулируются цель и основные задачи, решаемые в диссертационной работе.

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

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

Для реализации предложенных методов и алгоритмов анализа поведенче9 ских свойств РБ-сети формулируются матричные определения РБ-сетей, их маркировки и правил функционирования.

Для расширения возможностей анализа Р8-сетей вводится понятие ее базового подкласса — ВРБ-сетей, равномощного Р8-сетям, для которого предлагаются разработанные теоретико-множественное и матричное представления.

Подробно рассматриваются и описываются матричные уравнения над ВРБ-сетями и типы ее структурной определенности. Предлагается теория асинхронной интерпретации ВРБ-сети, в основе которой лежит теорема о решении уравнения СА-перехода, построенного для линейно и полулинейно определенной ВР8-сети. В рамках предложенной теории на основе введенных понятий БУЯ- и БО-инвариантов, предлагается метод анализа поведенческих свойств ВР8-сетей.

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

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

Для решения задачи преобразования ВР8-сети к ВР8-сети полулинейно определенного вида предлагаются алгоритмы БрИШреобразований.

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

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

10

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

Для анализа ПРПО на основе PS-сетей в рамках инструментальной системы моделирования «Parallax» созданы программные средства, предоставляющие пользователю следующие основные возможности: обнаружение в модели локальных тупиков; осуществление преобразований PS-сети к BPS-сети; построение дерева покрытий (достижимости) для PS- и BPS-сети; осуществление преобразований BPS-сети к BPS-сети полулинейно определенного вида; интерпретацию вариантов поведения приведенной BPS-сети; построение SVR- и SD-инвариантов.

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

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

Рассмотрена задача исследования корректности проектируемых способов организации распределенной обработки информации в «ГИС-сервере социально-экономической сферы субъекта федерации», разработанного по заказу Государственного научно-исследовательского института информационных технологий и телекоммуникаций «Информика» г. Москва. ГИС-сервер предназначен для организации удаленного доступа пользователей к функциям геоинформационной системы средствами Web-технологии и создавался в рамках разработки распределенной геоинформационной системы. Разработанные модели и результаты их анализа использованы при проектировании ПО ГИС-сервера. Так в частности, при анализе моделей PS-сетей на основе предложенных методов и алгоритмов были обнаружены ошибки в проектных решениях и предложены способы их устранения.

11

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

Научную новизну полученных в работе результатов определяют.

• формальные определения поведенческих свойств Р Б-сетей и методы обнаружения этих свойств, предназначенные для обоснования корректности проектируемого ПРПО;

• матричное представление аппарата Р Б-сетей, а также теоретико-множественное и матричное представления базового подкласса аппарата РБ-сетей — ВРБ-сетей, предназначенных для формального анализа поведенческих свойств описываемого на их основе ПРПО;

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

• теория асинхронной интерпретации ВРБ-сетей, опирающаяся на ряд теорем, доказанных автором, и позволяющая на основе решения уравнения СА-перехода расширить возможности анализа ВРБ-сети в части применения метода инвариантов;

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

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

Практическая ценность и реализация результатов работы. Практически значимыми являются созданные модели, методы, алгоритмы и программные средства для анализа проектируемого ПРПО на предмет его корректности. Программные средства функционируют на ПЭВМ типа IBM PC в операционной среде Windows 95/NT. Объем разработанного на языке С++ ПО составляет более 6500 строк программного кода.

Предложенные модели, методы и алгоритмы, а также разработанные программные средства анализа ПРПО были внедрены в Государственном научно-исследовательском институте информационных технологий и телекоммуникаций «Информика» г. Москва при проектировании и исследовании корректности способов организации распределенной обработки информации в проекте «ГИС-сервер социально-экономической сферы субъекта федерации», разработанного для использования в сети Internet. Эти же методы, алгоритмы и программные средства внедрены при исследовании верхних границ времени выполнения операций над данными пользователями «Регионального банка геологической информации по геологии нефти и газа и недропользованию» в многопользовательском режиме, разработанного в Западно-Сибирском геологическом научно-аналитическом центре г. Тюмень. Созданные программные средства анализа ПРПО также были внедрены в учебный процесс на кафедре Автоматизации проектирования Томского политехнического университета в составе инструментальной системы моделирования параллельных процессов «Parallax» при выполнении цикла лабораторных работ по курсу «Современные архитектуры вычислительных машин, комплексов, систем и сетей» и подготовке магистров. Результаты внедрений подтверждаются соответствующими актами.

13

Основные положения, выносимые на защиту:

1. Предложенные методы и алгоритмы анализа ПРПО позволяют исследовать его корректность еще на этапе проектирования.

2. Теория асинхронной интерпретации ВР8-сети существенно расширяет возможности анализа поведенческих свойств описываемого на их основе ПРПО.

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

4. Разработанные теоретические положения, методы, алгоритмы и программные средства позволяют проектировать надежное и эффективное ПРПО.

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

14

4.5 Основные выводы по главе

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

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

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

148 нию». На основе анализа моделей этого банка получены закономерности и сделаны выводы, послужившие базисом при принятии важных проектных решений, в частности, решения о выделении в составе банка отдельного компонента — абонентского пункта (пунктов). Результаты исследования также составили основу для разработки методологии эффективного использования этого банка данных.

4. Получены оценки временных затрат при решении задач анализа корректности конкретного ПРПО, демонстрирующие эффективность методов и алгоритмов анализа корректности ПРПО, описываемого на основе РЭ-сетей.

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

149

ЗАКЛЮЧЕНИЕ

Диссертационная работа посвящена созданию математического и программного обеспечения для анализа корректности ПРПО на основе аппарата PS-сетей. Получены следующие основные научные и практические результаты:

1. Сформулированы формальные определения, характеризующие поведенческие свойства PS-сетей при исследовании корректности описываемого на их основе ПРПО.

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

3. Разработаны теоретико-множественное и матричное представления базового подкласса PS-сети — BPS-сети. Создана теория асинхронной интерпретации BPS-сетей, опирающаяся на ряд доказанных автором теорем и направленная на расширение возможностей анализа ее поведенческих свойств в части использования метода инвариантов.

4. Разработан метод анализа поведенческих свойств BPS-сети, базирующийся на решении уравнения синхронно-асинхронного перехода и понятиях SVR- и SD-инвариантов, введенных в рамках предложенной теории асинхронной интерпретации BPS-сети.

5. Разработан ряд алгоритмов преобразований над PS- и BPS-сетями, позволяющих осуществлять приведение произвольной PS-сети к BPS-сети полулинейно определенного вида.

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

150 уточнение временных характеристик объектов модели при интеграции в нее разверток метадуг.

7. Созданы программные средства, реализующие предложенные методы и алгоритмы анализа корректности ПРПО, описываемого на основе PS-сетей. Разработанное ПО функционирует на IBM PC-совместимых ПЭВМ под управлением ОС Windows 95/NT и состоит из более чем 6500 строк программного кода на языке С++.

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

9. Разработанные методы, алгоритмы, программные средства, модели и результаты исследований моделей внедрены в Государственном научно-исследовательском институте информационных технологий и телекоммуникаций «Информика» г. Москва и в Западно-Сибирском геологическом научно-аналитическом центре г. Тюмень. Программные средства анализа ПРПО также внедрены в учебный процесс в Томском политехническом университете.

1. Agerwala Т., Flynn М. A Complete Model for Representing the Coordination of Asynchronous Processes. — In: Hopkins Computer Research. Report 32. Baltimore, 1974.

2. Alur R, Courcoubetis C., Dill D. Model-checking for Real-time systems. Proc. 5*1 IEEE LICS, 1990, p. 214-225. AlurR., DillD. The Theory of Timed Automata. Lect. Notes Comput. Sci. — 1991. — Vol. 600. — p. 45-73.

3. Boudol G., Castellani I. On the Semantics of Concurrency: Partial Orders and Transition Systems // Lect. Notes Comput. Sci. — 1987. — Vol. 249.—p. 123-137.

4. Boyer R.S., Moore J.S. Computation Logic Handbook. Academic Press, Volume 23 of Perspectives in Computing, 1988. Brams G.W. Reseaux de Petri: Theorie et Pratique. V. 1-2. Paris: Mas-son, 1983.

5. Clarke E.M., Emerson E.A., Sistla A.P. Automatic Verification of Finite-State Systems Using Temporal Logic Specifications. ACM TOPLAS 8(2), 1986, p. 244-263.

6. Courtois P.J., Heymans F., Parnas D.L. Concurrent Control with Readers and Writers. — Communs ACM, 1971, vol. 14, № 10, p. 667668.

7. Czaja L. A Calculus of Nets // Кибернетика и системный анализ. — 1993, —№2, —с.40-50.

8. GenrichH. J., Lantenbach К., ThiagarajanP.S. Elements of General Net Theory // Lect. Notes Comput. Sei. — 1980. — Vol. 84. — p. 21163.

9. Ghezzi C. Concurrency in Programming Languages: a Survey // Parallel computing: 1985. — № 2. — p. 229-241.

10. Gilbert P., Chandler W.J. Interference Between Communicating Parallel Processes. — Communs ACM, 1972, vol. 15, № 6, p. 427-437.

11. Harel D. Biting the Silver Bullet // IEEE Computer. 1992. — Vol. 25. — № 1,—p. 514-520.

12. HenzingerT.A., Manna Z., PnueliA. Timed Transition Systems. Lect. Notes Comput. Sci. — 1991. -—Vol. 600. — p. 226-251. Holt R.C. Some Deadlock Properties of Computer Systems. — ACM Comput. Surv., 1972, vol. 4, № 3, p. 179-196.

13. Karp R., Miller R. Parallel Program Schemata, RC-2053, IBM T.J. Watson Research Center, Yorktown Heights, New York, 1968, pp. 54. Katoen J.P. Qualitative and Qualitative Extensions of Event Structures. PhD Thesis, Twente University, 1996.

14. Markov N., Ostrast P. Distributed Web-based GIS, Proc. 2nd AGILE Conference on Geographic Information Science, Rome, Italy, April 1517, 1999, p. 53.

15. Markov N.G., Miroshnichenko E.A., Sarajkin A.V. Analysis of Parallel Computation Correctness With the Use of PS-nets // In: Abstracts of the 2nd Korea-Russia Int. Symp. on Sei. and Tech. — Tomsk, TPU, 1998.—p. 253.

16. Markov N.G., Miroshnichenko E.A., Sarajkin A.V. Method and Tools for Parallel and Distributed Software Creation // In: Proceedings of the 1st Korea-Russia Int. Symp. on Sei. and Tech. — Ulsan, Ulsan University, 1997. — p. 389-394.

17. Markov N.G., Miroshnichenko E.A., Sarajkin A.V. Method and Tools for Parallel and Distributed Software Creation // In: Abstracts of the 1st Korea-Russia Int. Symp. on Sei. and Tech. — Ulsan, Ulsan University, 1997,—p. 205.

18. Markov N.G., Miroshnichenko E.A., Sarajkin A.V. Technology of Design of Distributed Applications with the Use of PS-nets // Join Bulletin of NCC and IIS, Series Computer Science, Novosibirsk. — №12, 1999, —p. 32-36.

19. Milner R. A Calculus of Communicating Systems // Lect. Notes Comput. Sei. —1980.—Vol. 92.

20. Nielsen M., Plotkin G., Winskel G. Petri Nets, Event Structures and Domains // Theoretical Computer Science. — 1981. — Vol. 13. — p. 85-108.

21. Nielsen M., Thiagarajan P.S. Degrees of Non-determinizm and Concurrency: A Petri Net View // Lect. Notes Comput. Sei. — 1984. — Vol. 181. —p. 89-117.

22. Noe J.D., Nutt G.J. Macro E-nets for Representation of Parallel Systems // IEEE Trans. Computers, Aug. — 1973. — Vol. C-22. — p. 718727.

23. Ostroff J.S. Temporal Logic of Real-time Systems. Research Studies Press, 1990.

24. Park D. Concurrency and Automata on Infinite Sequences // Lect. Notes Comput. Sei. — 1981. — Vol. 104. — p. 167-183. Patil S. Coordination of Asynchronous Events. — Massachusetts, June 1970, —234 p.

25. Petri C.A. Kommunikation mit Automaten. — Technische Hochschule Darmstadt, 1962.

26. Plotkin G. An Operational Semantics for CSP // Formal description ofprogramming concepts. II. N.-H. Press, 1983. P. 199-223.

27. Pomello L. Some Equivalence Notions for Concurrent Systems. Anoverview//Lect. Notes Comput. Sci. — 1986. — Vol. 222. — p. 381—400.

28. Schneider S., Davies J., Jackson D.M., Reed G.M., Reed J.M., Roscoe A.W. Timed CSP: Theory and Practice. Lect. Notes Comput. Sci. — 1991. — Vol. 600. — p.640-675.

29. Sinachopoulos A. Partial Order Logics for Elementary Net Systems: State- and Event Approches // Lect. Notes Comput. Sci. — 1990. — Vol. 458.

30. Valk R. On the Computational Power of Extended Petri Nets // Lect. Notes Comput. Sci. — Berlin: Springer-Verlag, 1978. — Vol. 64. — p. 526-535.

31. Valk R. Self-modifying Nets, a Natural Extension of Petri Nets. — In: Lect. Notes Comput. Sci. — Berlin: Springer-Verlag, 1978. — Vol. 62. — p. 464-476.

32. Van der Aalst W.M.P. Interval Timed Coloured Petri Nets and Their Analysis // Lect. Notes Comput. Sci. — 1993. — Vol. 691. — p. 453472.

33. Van Glabbeek R.J., Vaandrager F. Petri Net Models for Algebraic Theories of Concurrency // Lect. Notes Comput. Sci. — 1987. — Vol. 259.—p. 224-242.

34. Vogler W. Bisimulation and Action Refinement // Lect. Notes Comput. Sci. — 1991. — Vol. 480. — p. 309-321.

35. Wang F. Timing Behavior Analysis for Real-Time Systems. Proc. 10th IEEE LICN, 1995, p. 112-122.

36. Алгоритмы, математическое обеспечение и архитектура многопроцессорных вычислительных систем / Под ред. А.П. Ершова. — М.: Наука, 1982. — 336 с.

37. Ачасова С.М., Бандман O.JI. Корректность параллельных вычислительных процессов. — Новосибирск: Наука. Сиб. отд-ние, 1990. 253 с.

38. Бандман О.Л. Поведенческие свойства сетей Петри (обзор французских работ) // Известия АН СССР, Техническая кибернетика, 1987, № 5, с. 134-150.

39. Барский А.Б. Параллельные процессы в вычислительных системах. Планирование и организация. — М.: Радио и связь, 1990. — 256 с.

40. Вотинцева A.B. Методы спецификации и анализа параллельных процессов, представленных структурами событий: автореферат диссертации на соискание ученой степени к.ф-м.н. Новосибирск. — 1997, — 16 с.

41. ГИС-сервер Социально-экономической сферы Томской области. — http : Wee. cctpu. edu. ru\gis\

42. Йодан Э. Структурное проектирование и конструирование программ: Пер. с англ./Под ред. Л.Н.Королева. — М.: Мир, 1979. 416 с.

43. Котов В.Е. Сети Петри. —М.: Наука, 1984. — 158 с.

44. Липаев В.В. Качество программного обеспечения. — М.: Финансыи статистика, 1983. — 264 с.

45. Липаев В.В. Проектирование программных средств. — М.: Высш. шк., 1990,—303 с.

46. Майерс Г. Искусство тестирования программ: Пер. с англ. — М.: Финансы и статистика, 1982. 178 с.

47. Мирошниченко Е.А. Четырехэтапная технология создания параллельного программного обеспечения // Кибернетика и ВУЗ. — 1999. — Вып. 29. — с. 126-136.

48. Покозий Е.А. Методы спецификации и верификации параллельных моделей с непрерывным временем: диссертация на соискание ученой степени кандидата физико-математических наук. Новосибирск, ИСИ СО РАН. — 1999. — 76 с.

49. Сарайкин A.B. Сравнительный анализ моделирующей мощности PS-сетей и классических сетей Петри // Кибернетика и ВУЗ. — 1999. — Вып. 29. — с. 83-94.

50. Смелянский P.JI. Вестник Моск. Ун-та. Сер. 15. Вычисл. матем. и Кибернетика. 1990. № 3. с.3-18.

51. Тарасюк И.В. Алгебра AFLTV исчисление помеченных недетерминированных параллельных процессов// Проблемы спецификации и верификации параллельных систем. — Новосибирск. — 1995, —с. 22-49.

52. Уваров В.В., Хафизов Ф.З., Шаталов Г.Г. Опыт создания регионального банка цифровой геологической информации: Материалы Межрегиональной конференции. — Томск: ГалаПрес, 2000. — Том 2.— с. 428-430.

53. Устименко А.П. Отображение временных причинно-следственныхструктур во временные сети Петри // Кибернетика и системныйанализ. Киев, 1997, № 2, с. 44-54.

54. Фейс Р. Модальная логика. — М.: Наука, 1974. — 520 с.

55. Хоар Ч. Взаимодействующие последовательные процессы: Пер. сангл. — М.: Мир, 1989. — 264 е., ил.

56. Шоу А. Логическое проектирование операционных систем: Пер. с англ.—М.:Мир, 1981. — 360 с. ил.161