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

2 10 Ъ

о г ■

ЛЕЙИНГРЛдаКИИ .ОРДЕНА ЛЕНИНА И ОРДЕНА ОКТЯБРЬСКОЙ РЕВОЛВДИИ ЭЛЕКТРОТЕХНИЧЕСКИЙ ИНСТИТУТ ИМЕНИ ЕЙ.УЛЬЯНОВА (ЛЕНИНА)

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

: , УРСУ Анатолий Георгиевич

ИОСЛЕДОВАНИВ И РАЗРАБОТКА ВЗАИМОДЕЙСТВИЯ ПРОГРАШ В АСУ НА <ХЗШВЕ СПЕЩШКА1Ш ТЕМ1ЮРАЛЬЮ51 логики •

Специальность: 05.13.06 - Автоматизированные системы^

управления .'; - •

05.13.11 - ^тематическое и программное обеспечение вычислительных ' машин и систем . • • ' • 1

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

Ленинград -1990

Работа выполнена в Лениградскоы ордена Ленина и ордеда Октябрьской Револвции, электротехническом институте имени В.И.Ульянова (Ленина)

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

кандидат технических наук доцент Дубенецкий В.А. Официальные оппоненты:

доктор технических наук профессор Сизов В.Е. кандидат технических наук доцент Хохловский В.Н.

Ведущая организация - Киевский политехнический институт, имени 50-летия Великой Октябрьской социалистической революции/

Защита состоится " " ¡р1990 г. в

/ОС/Э часов на заседании специализированного совета К 063.36,03 Ленинградского ордена Ленина и ордена Октябрьской Революции ' . электротехнического института имени В,И.Ульянова (Ленина).по адресу:' 1370132, Ленинград, ул. Проф. Попова, 5.

С диссертацией можно ознакомиться в библиотеке института.

• • V '-< ' "

Автореферат разослан " <Г " ОО^¿Ь-/1990 г.

Ученый секретарь специализированного ..совета

Кутузов"О,И.

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

Актуальность пробяем'н. Современный этап развития научно-технического прогресса н народнохозяйственного комплекса страны характеризуется необходимостью все более широкого использова-ния'ггри решении народно-хозяйственных задач услуг систем автоматизированной . обработки ишормации и управления. . В этих условиях особую оотроту приобретают вопросы формализации и автоматизации разработки программного обеспечения /ПО/ на,основе |£ункционачь-' Них спецификаций проектируемых.автоматизированных систем управления /АСУ/. •

Анализ тенденций развития современных АСУ и , э частности,' АСУ гибкими производственными системами /ГОС/ приводит К выводу, что для таких систем характерна децентрализованная структура управления, многофункциональноегь ПО а распределенный характер обработки информации. В силу указанных особенностей ПО такюс' систем реализуется в виде многозадачного программного обеспечения, аадачи которого, взаимодействуют олотаым' образом между собой я с окружение?.!. Наличие сложного информационного взаимодействия ые*-ду- задачами в процессе функционирования предъявляет высокие требования к процессу разработки и анализа корректности взаш.:одействия программ в АСУ.

'■■-" Перспективна направлением разработки многозадачного ПО АСУ является разработка взаимодействия программ на основе спецификаций допустимых временных последовательностей.событий взаимодействия. При нтом конструктивным аппаратом представления и .логического анализа спецификаций допустимых последовательностей' событий взаймо'действия программ . является аппарат- темпоральной логики /ТЯ/. ' . ;•

Указанные особенности ПО АСУ, с одной стороны, и перспёктив-ный похреод разработай взаимодействия программ, о другой стороны, позволяют-сформулирЬвать требования к процессу разработки взаимодействия Программ в АСУ/основным из которых: является обеспечение возможности синтеза автоматных моделей взаимодействия -программ на. основе спецификаций допустимых последовательностей- событий''на языке темпоральной логики.' ■ '•• . .

-Вопросам.. разработки, и анализа ' корректности ПО.на основе

спедайЕшсаций посвящен ряд работ советских и зарубежных авторов. Среда них можно вы целить статьи к монографии В.Н. Агафонова, ' Е.Л. Ющанко, В.Д. Ильина, Э.Х. Гнуту, В.А. Непомнящего, Б. Лескова, Ч. Хоара, П. Бахманна, К,Р, Апта, Н. Франкеза, Б. Хэлпврна, С, Овики, Е.М. Кларка, Е.А. Эмерсона, Л. Лэмпорта, 3. Манны, А. Пнуэлн, Е.-Р. Олдерога, В.Р. да Ревера, II. Волпера и др. Несмотря на значительное чис^о работ, проблема синтеза автоматных, моделей взаимодействия программ в АСУ на основе спецификаций до-оустшых последовательностей собнтий взаимодействия программ и' анализа корректности их информационного взаимодействия остается не решенной.. • -

В связи с этим, исследование и.разработка методов и средст! взаимодействия программ в АСУ.представляет собой актуальную задачу, важную как с научной, так и с практической точек зрения.

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

В соответствии с указанной целью в работе поставлены и решены слелуэдие задачи. ■ '

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

2. Разработка метода синтеза автоматных моделей взаимодействия программ в АСУ на основе спецификаций темпоральной логики с применениш процедуры анализа выполнимости формул спецификаций

т....... Г .•' , :■;■■■/.;■':•■' .-•/■•.. '..-..

3. Создание методики разработки взаимодействия программ и анализа корректности их информационного взаимодействия на основе спецификаций темпоральной логики.

4. Разработка спецарикадай темпоральной логики взаимодействия процессов системы управления участком ГПО,

:5.:Ра&ра5отка автоматной модели взаимодействия процессов систему управления .участком ШС на основе применения .процедуры •

строения модельного графа формул спецификаций темпоральной ло-ки. .

Методы исследований. При проведении исследований в диссерта-. онной работе использованы"положения и методы классической мате-.тической логики, темпоральной логики, теории автоматов, формаль-ас языков, аппарата Алгебраических спецификаций, взашэдеПствут.-х последовательных процессов Ч. Хоара, теоретического программ«-|вэния, теории графов. .

Новые научные результаты. '■

1. Формализм представления и логического анализа,специфика-!й допустимых последовательностей событий взаимодействия программ АСУ на основе аппарата темпоральной логики А. Пнуэли, отличай-, ¡йен использованием вложенных темпоральных операторов "пока" и:

: тех пор", позволяющий описать временные свойства взакмодсйст-' 1Я программ за счет.семайтики темпоральных операторов.:

2. Метод синтеза автоматных моделей взаимодействия программ АСУ на основе спецификация темпоральной логики, отличающийся . »строением модельного графа спецификаций на основе процедуры ана-!за выполнимости; формул темпоральной логики П.Болпера-З.Майны, ■ ззволяющий алгоритмизировать синтез автоматных моделей как на знове спецификаций допустимыхпоследовател" гостей событий взаамо-эйствия, так. и на основе спецификаций допустимых поаледователь--эстей состояний взаимодействующих программ за счет однотипности роцедура анализа выполнимости формул спегификаций временных пос-эдовательно'отей на языке темпоральной логики..

3. Методика разраббтки и анализа корректности взаимодействия рограмм в АСУ, отличающаяся 'формализацией основных этапов пос-роения спецификаций и анализа их корректности на основе апнара-а темпоральной логики к. алгебраических"спецификаций, разработкой втоматной модели взаимодействия программ, позволяющая проектиро-ать логику синхронизационной части программ за счет построения окальных автбиатных моделей и уравнений перехода.

.4,- Спецификации взаимодействия процессов системы управления частком механообработки Л1С на языке темпоральной логики,. от-ичающиеся модульностью, полнотой л непротиворечивостью описания опуст'имых последовательностей событий взаимодействия,' о'беспе-• иваа'щйе построение автоматной модели взаимодействия процессор.

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

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

1 Практическая ценность. Практическая ценность результатов р 'боты состоит в следующем.

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

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

ционной среде ОСРБ 3.1 Сш-1420.

Реаяизатая в промыпшенности. Исследования и разработки, ви полненные, в диссертационной работе, являются частью хоздоговора ных научно-исследовательских работ» проводимых на кафедре Автом тизированных систем обработки информации и управления Ленинград ского ордена Ленина и ордена Октябрьской Революции электротехни чёского института имени В.И.Ульянова (Ленина) и использованы в ЛШЮ "Электронмаш" и на электромеханическом заводе "Буревестник г.: Гатчина. Гарантированный годовой экономический эффект, от использования результатов работы составляет 31 тысячу рублей.

' Апробация работы. Основные положения и.результаты диссёрта шинной работы были изложены и обсуждались-на:

- XI Всесоюзном совещании по • проблемам управления "Проблем управления - 89" /Ташкент1989/;

„- Всесоюзном научно-техническом семинаре "Мобильное програ шое обеспечение" /Калинин, '1988/$' •■ ...

- Всесовзной научно-технической конференции "Конструкторе»

эхнологическая информатика, автоматизированное создание машин и зхнологий КТИ - 89" /йосква, 1989/; . - . ' .

. - Третьем региональном семинаре "Распределенная обработка нформаяии" /Улан-Удэ, 1980/; ;

- Региональной'научно-технической конференции "Перспективные вправления развития автоматизированных систем управления и их омпонентов" /Омск, 1989/;

- Республиканской научно-технической конференции "Проблемы втоматйзании перенастраиваемых производств в машиностроении" Волгоград, 1988/; ■ , - • .

- Научно-технической конференции "Проблемно-методические и ¡роградано-тёхнйческие комплексы САПР и АСТШ" /Иаевсй,,1988/;

- Научно-технической конференции "Цифровые методы в решении 1ацач управления" /Днепропетровск, 1989/;

- Научно-технических конференциях профессорско-преподаватель-!К0Г0 состава ЛЗТИ ш/еки В.И.Ульянова /Ленина/ в 1987 - . ■ .990 гг. .

Публикации. По материалам диссертационной работы опубликовало- 7 печатных рабоа. .' •'■ * '

• ..Структура Я объемоаботн. Диссертационная работа состоит из-зведен'ия, четырех глав с выводами, заключё ш, списка литературы I пяти приложений. Основной текст работы изложен на 149 страницах .машинописного текста,, содержат 17 рисунков, 4 таблицы.-Список литературы включает 151 наименование.

• -КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ -.'

-Во введении обосновывается актуальность, проблемы^ формула-руютя цель и.задали диссертаияояпой работы, приводится ее краткое содержание^ ' . , г ' ■ • В первой главе Рассматриваются особенности автоматизированных систем управления,' дается общая характеристика программного обеспечения "АСУ, характеристика проблемы разработка взаимодействия программ в АСУ, приведен обзор существугарх методов, й средств разработки ПО АСУ,'ставится и формулируется задача разработки взаимодействия.программ в АСУ на основе спецификаций допустголых послёдовательностей событий взаимодействия

на языке темпоральной логики.

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

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

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

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

- расширенные конечные автоматы; . - сети Петри; \

- аппарат CSP взаимодействующих последовательных процессо Ч. Хоара; . '

. . - исчисление С С S взаимодействующих систем Р,'Мйлнера;

- .темпоральная логика А.. Пнуэли; ' ■

.:' Рассмотрены преимущества и недостатки перечисленных средств из которых'следует несовершенство; первых четырех средств в • чистом ви-:в применительно л .задаче разработки взаикодейотвия

oneccoD и целесообразность использования темпоральной логики в яестве формального средства описания л логического анахпза взаи-действия. Предложено использовать.сочетание■различных формата»- . ос средств анализа на разных этапах разработки- Б качестве сред-ва'представления логики взаимодействия процессов предложено пользовать расширенные конечные автоматы, для которых существуют лее.развитые по сравнению с сетями Пегри-способы ..ерехояа ст. афического задания логики к программному. G использованием ко-1чных автоматов задача синтеза логики взаимодействия процас'сов" '. юдится к задаче синтеза автоматной модели взаимодействия гк> ло-[чёскш^ спецификациям. В качестве языка спецификаций взаимоцей-■вия программных - процессов прадложечо использовать формальный ... шарат темпоральной логики, который обладает большей универсалЬ-icibD по.сравнению с языкгмй CSP и CCS и большими вырази--»льнами возможностями по сравнения о языком спецификаций логика >едияатов первого порядка.

Во второй главе проводится исследование продуктивных авто- . йных моделей применительно к задаче разработки взаимодействия юграммнык процессов, рассматривается аппарат темпоральной логи-[ в качестве основы формализма спецификации взаимодействия про-iccob,: предложены алгоритм« разработки спе**и$йкадмй взажюдейст-1я процессов .на языке темпоральной логики , алгоритм анализа кор-жтности взаимодействия и Met од синтеза автоматных моделей- взаи-щействия . процессов на основе спецификаций темпоральнойлоги-I.. V; - . ,' . •."'"■' ..'.-.■•■• /

Продуктивные;автоматные модели.являются расширением тради-юнных автоматных моделей условия?«! сильной и слабой пролуктив--юти, при недетерминированном, выполнении переходов автоматов. .-. ;ловия продуктивности гарантируют сыполнение специфицируемых ими. феходов автоматных моделей прл неоднократной или непрерывной их (товности к выполнению.. Предложены продуктивные автоматные моде-I для: а/ взаимодействующих процессов с общей памятью; б/ про-!ссов, взаимодействующих с помощью механизма-сообщений синхрон-га. способом; в/ процессов, взаимодействующих с помощью механизма юбщений асинхронным способом. / . : •

: Программная система Р "-/ состоящая йз it взаимодействующих зограмм, представляется срвотоганостью процебсоз P-U) (if i'r^),

функционирующих параллельно и взаимодействующих между собой и с окружением, т. е.- в виде следующей параллельной композиции!

р=А||рЛец... 11 Ра,

где Л - оператор параллельной композиции.

Выявлено, что такие системы описываются продуктивными авто-маткнми моделями, для них характерно недетерминированное поведение и описание их взаимодействия невозможно только с помощью троек Хоара {д) р {0} . т, е. в терминах предусловий Я постусловий 0-,

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

(Г; аг-^а*-^ ... ^й/Ди..

где 0.1 - состояние системы, определяемое значениями программны переменных; Т1 - собитие /переход/, переводящее систему из те щего состояния йс в слепуадее состояние йI . При разработ Взаимодействия процессов событиями *Гг являются события взаим действия, т. е. события приема/передачи сообщений.

В диссертационной работе пш слагается использовать аппарат темпорааьной логики А. Пнуэли для описания временных послецова тельностей событий и состояний при разработке логических специ$ каодй взаимодействия процессов. 3 качестве основы языка сиецифи каций предлагается использовать подмножество темпоральной логик а именно, пропозициональную темпоральную логику /ПТЛ/, которая представляет собой расширенна традиционной логики исчисления высказываний темпоральными операторами будущего и прошедшего -вр мени: □ '- "всегда", О' - "когда-нибудь", О -"следующее - "пока", и - "сильное пока", □ - "всегда в прошлом 0 - "иногда в ■прошлом"-', 0 • - "предыдущее", 3 - "с тех пор", «5 - "сильное с тех пор".

Если /< и 1/г являются формулами классической, логики, а Утверждение о будет-истино, если истина в..текущий мои и во .г.ре моменты времени, посла дующие текущему;-О ' 'истино,

если Ji будет истина в- некоторый момент времени в будущем; О^* истино, если Ji истина в следующий момент времени; JiUJi истино, если Ja будет истина всегда в будущем или Jz .будет истина в некоторый момент времени в будущем и до этого момента истина J< ; J-tVJi истино, если существует такой момент времени в будущем, корда Jz истина и до этого момента истина Ji Аналогично определяется семантика операторов прошедшего времени относительно времени в прошлом.

Исследованы.выразительные^свойства формул ПТЛ. Проведена классификация, свойств,, выразимых формулами Г1ТЛ.' На основе выражения канонического разложения формул темпоральной логики,

хм ( aoSi v О о d-i),. выделены возможные подформулы, которым соответствуют следующие свойства: □ £ - "безопасность", OJ - "живучесть", □/v О <£ -"альтернативность", fo (aJi v о cLl) - "глобальная альтернативность", О о/ - "отзывчивость", Оо $ - "настойчивость", о QJ v О Q d - "развиваемость",ЯГ<Г°0^' voa di) "глобальная развиваемосгь", где. Ji± dcjt= f, л-) - формулы темпоральной логики прошедшего времени.

■ Для представления произвольных временных последовательностей с фиксированным порядком следования событий предложены сиециаль-. ныв конструкции вложенных'темпоральных операторов "пока" и "с тех'пор"': • >-'

ЛиЛ Vh V. •. VJn. 3 -Jt и(/г V . •. vjw)...), Ji SJz5... SJn, 2 J, J(JzS '. v. • • •),

■ семантика которых определяет следующий временной порядок истинности, формул Л,/»,. Jn- относительно будущего времени, в первом случае и относительно прошедшего - во втором: если-в некоторый момент времени истина формула , в следующий момент ис-. тина некоторая формула Jj , где i ¿j 4 ^ •

Рассмотрены алгоритмы разработки спецификаций в рамках фор- мализма ПТЛ для конкретных примеров взаимодействия процессов.

Предложен алгоритм анализа корректности взаимодействующих процессов на основе развития метода индуктивных утверждений

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

Алгоритм отличается:

а/ особыми спецификациями процессов вида:^]"^"/} , для которых в отличие от традиционных троек Хоара не требуется знание программной логики специфицируемого процесса Р и семантика которых определяется импликациями ¡вида:

[у(а) л о! е тМ) — У(а!),

где С _ переход процесса Р ; .у", V - пред- и постусловия перехода С ; О., о! - состояния процесса' до н после выполнения перехода <Г ;

б/ правилом инварианта для доказательства свойств корректности

н- Я — Ч .

ь- М т №

Н- а У '

где Т множество всевозможных переходов процесса Р у определяемое на основе продуктивной' автоматной модели; Ц - предусловие процесса.

В диссертационной работе предлагается метод синтеза автома ных моделей взаимодействия процессов на основе спецификаций на языке ПТЛ, который отличается от-известных методов Е.М. Кларка-Е.А. Эмерсона, П. Волпера - 3. Канны, Е.-Р. Олдерога тем, что позволяет синтезировать автоматные модели взаимодействия'какда .основе спецификаций допустимых последовательностей событий, взал-■модействия,, так и на основе спецификаций -допустимых последовательностей состояний процессов. В основу метода положена процедура анализа выполнимости формул ПТЛ, основанная на декомпозтр» ■формул ПТЛ на формулы текущего'состояния /формулы классической /логики- / и формулы следующего состояния'/формулы ПТЛ,-предва- ■ ренине оператором. О /.

.Процедура декомпозиции и анализа выполнимости формул ПТЛ используется, для построения модельного графа формул спецификавдп

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

Исходными данными для процедуры декомпозиции и анализа выполнимости является исходное множество формул 21 и некоторая логическая переменная спецификаций ^ > значение которой принимается истинным. Результатом выполнения процедуры является множество подмножеств формул темпоральной логики, т. е.

'2»-' 1 • • • где Ы - формула

спецификаций. Множества г^ состоят из формул следующего состояния.

Процедура построения модельного графа состоит в выполнении следующих шагов:

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

а/ применить процедуру декомпозиции множества формул рассматриваемого узла при истинном значении ^ . ;

б/ для каждого подмножества множества ^ , полученного в результате применения процедуры декомпозиции, создать дугу, помеченную множеством формул О \ с началом в . текущем узле и концом в.узле, помеченном множеством формул ; если таких узлов нет создать новы;1!.

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

Третья глава посвящена разработке функциональных -спецификаций программного обеспечения системы управления участком механообработки ГПС на языке описания графо-иерархичёских структур, .логических спецификаций взаимодействия процессов программного обеспечения'системы управления участком на языке темпоральной логики, глобальной автоматной модели протокола взаимодействия процессов системы управления на основе спецификаций темпоральной

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

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

• Процесс проектирования ПО системы вз'аишдействующих'про-цессов системы управления участком представлен в виде двух . взаимосвязанных этапов:

а/ проектирование функциональной части процессов на основе функциональных спецификаций;

.6/ проектирование синхронизационной части процессов /логики взаимодействия/ на основе логических спецификаций взаимодействия.

Разработаны логические спецификации взаимодействия процессов системы управления участком.В процессе взаимодействия один процее выступает в роли главного, другой-в роли подчиненного. Обозначим их соответственно ГУ и ПУ. В качестве элементарных действий взаимодействия главного и.подчиненного процессов вараны следующие действия: П0СЛАТЬ_1У, ПОСЛАГЬПУ, ПРИНЯТЬ_ГУ, .ПИШШЪ_ПУ, т. е. действия передачи и приема сообщений'соответственно главным и подчиненным процессами. Спецификации взаимодействия процессов ГУ. и ПУ Составлены в терминах следующих событий готовности . выполнения действия взаимодействия: послать_ГУ, цослать_ПУ, ■принять_ГУ, принять_ПУ. '_*

.. Получены следующие^обобщенные спецификации взаимодействия процессов ГУ и ПУ на языке ПТЛ: '

Т лроцесс_1У U нослать_ГУ; ' '

О /пр;шять_ГУ -* О/'1 процесс_ГУ Ú послать_1У//; '

Тпроцесс_ПУ U послать_ПУ;

□ /принять_ПУ -»■ 0/-|процесс_ПУ Ü лослать_ПУ//;

;а/послать_ГУ — O/i принять_ГУ V послать_ПУ//;

, D /послать _ПУ — о/~\ дринять_ПУ U поСлать„ГУ//У. О ф/процесс_ГУ/; D О /процесс_ПУ/; . •

О /послать_ПУ т» О / т послать_1и//; □ /послать_ГУ о /1 послать_ГУ//; Й /послать_1У О /послать_ПУ V "] послать_ГУ//; а /послать_ПУ — о /послать_ГУ V -] послать_ПУ//; лроЦесс_ГУ = послать_ГУ V принять_ГУ; процесс_ПУ = послать_ПУ У принять_ПУ.

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

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

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

Четвертая глава посвящена разработке инструментального и методического обеспечения процесса разработки спецификаций, проектирования и отладки, взатлодействия процессов ПО 'АСУ.

Реализован инструментальный комплекс автоматизации разработки " •' функциональных спецификаций ИКАРС для автоматизированной поддержки, процесса построения спецификаций п их логического анализа' на основе совокупности взаимосвязанных моделей "представления, проектов ПО АСУ: функциональная модель, модель данных, модель логики модулей, модель структуры модулей, ■

Описан комплеко разработки и анализа корректности информационного взаимодействия процессов ПО АСУ, взаимодействующих

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

Разработан пакет программных средств взаимодействия прогпамм предоставляющий разработчикам многозадачного ПО АСУ адап©Добные средства взаимодействий программ на языке Паскаль*

Предложенные средства разработаны на языке Паскаль в операционной среде ОСРВ 3.1 С},1-1420.

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

Проведено экспериментальное исследований предложенных средств и анализ ах эффективности согласно методики.ГОСТ 28135-89 "Оценка качества программных средств"Анализ показал целесообразность использования предложенных средств в качестве инструментального и методического обеспечения процесса разработки . взаимодействия программ в АСУ.

ОСНОВНЫЕ РЕЗУЛЬТАТЫ РАБОТЫ

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

. ;;; .' 2." Предложен мегод синтеза автоматных моделей взаимоце^сгрн "программ в-АСУ на.основе спецификаций те,¿¡хоральной логики,

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

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

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

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

6. Разработаны инструментальный комплекс автоматизации раз-©ботки спецификаций ИКАРС, позволяющий автоматизировать процесс «строения спецификаций и их логического анализа, 'и комплекс раз-юботки и анализа корректности информационного взаимодействия (рограмм, позволяющий в интерактивном режиме проводить разрайот-у и отладку взаимодействия программ многозадачного. ПО АСУ. ■ .

7. Реализойая пакет программных средств взаимодействия про-'рамм, предоставляющий разработчикам многозадачного ПО АСУ ада-юдббные средства взаимодействия программ на языке Паскаль .

I операционной среде ОСРВ 3.1 №-1420.

• ПУБЛИКАЦИЙ по таи .ДИССЕРТАЦИИ . :: ■ .'•.;.

1. Дубенешшй В.А., Урсу А.Г. Методологическая и инотрумен-..

талвная поддержка процесса проектирования'программного обеспечен« систем правления ГПС//Гез. докл. Всес. науч.-техн. конф. "Конс-трукторско- технологическая информатика, автоматизированное созда ние машин и технологий КТИ - 89", март 1989.-М. :РЧШТЭШР, 1989. -С.24.

2. Дубенецкий В.А., Урсу А.Г. Обеспечение мобильности програ много обеспечения ГЛС на язцке Паскаль с помощью механизма взаимо действия з'адач//Тез. докл. Всес. науч.-техн. семинара "Мобильное: программное обеспечение", 22-24 ноября 1988.-Калинин:Центрпрограл систем,'1988.-4.1.-С.67-68.

3. Дубенецкий В.А., Урсу А.Г. Проектирование взаимодействия задач программного обеспечения ГПС//Тез. докл. Республ. науч.-тех конф.. "Проблемы автоматизации перенастраиваемых производств в мал ностроении", 16 ноября 1988.-Волгоград, 1988.-С.80-81. .',

4. Дубенецкий В.А., Урсу А.Г., Петров Д.Е. Автоматизация прс ектирования функциональных спецификаций программного обеспечения АСУ реального времени//Тез. докл. Регион, науч.-техн. конф1. "Перспективные направления развития автоматизированных систем"управл« ния и их компонентов", 12-13 октября 1989.-Омск:ОмПИ, 1989.-С.25.

• 5. Дубенецкий В.А., Урсу А.Г., Петров Д.Е. Разработка программных средств взаимодействия задач программного обеспечения сис тем управления реального. времени//Гез. докл. Третьего регион'альнс го семинара "Распределенная обработка .информации", 2-6 июля.1989. -Новосибирск, 1989.-С.32. ■ . ; '.

• ' 6. Урсу А.Г. Методологическая и инструментальная поддержка • процесса проектирования программного обеспечения ГПС//Проблемы с! темотехники и АСУ: Мелеву з. сб. науч.'тр. -Л.:СЗПИ, 19У0.-СЗ-.&Э-62.

7. Урсу А,Г. Проектирование структуры программного обеспечо! АСУ на базе аппарата■ теории гиперграТовХ/Тез. докл."XI Всес.' сов< щания по проблемам управления "Проблемы управления 89'', 25-30 се! тября' 1989.-:.'!. :ВЩТИ, 1989.-С.303-304. ',"' .';/''.

ПодаЦйпеч. 28.09.90. Формат 60x84 1/16 " Офсетная печать. Печ. л. 1.0; уч.-изд.л. 1.0. Тираж 100 экз. Зак. №304 . Бесплатно.

;■'■• // - Ротапринт ЛЭТИ ■■ ■ . . 197022,' Ленинград, -ул.. Проф.. Попова, 5 ■ ~