Введение к работе
Актуальность проблемы. Современный этап развития научно-
технического прогресса и народно-хозяйственного комплекса стра
ны характеризуется необходимостью все более широкого использова-
ния'при решении народно-хозяйственных задач услуг систем автома
тизированной . обработки иніормации и управления..В этих условиях
особую оотроту приобретают вопросы формализации и автоматизации
разработки программного обеспечения /ПО/ на,основе функцион&яь-'.
них спецификаций проектируемых.автоматизированных систем управле
ния /АСУ/. ' '
Анализ тенденций развития современных АСУ и , g частности,' АСУ гибкими производственными системами /ГОС/ приводит К выводу, что для таких систем характерна децентрализованная структура управления, многофункциональность ПО а распределенный характер обработки информации. В силу указанных особенностей ПО таких' систем реализуется в виде многозадачного програмшюго обеспечения, аадачи которого, взаимодействуют олотаым' образом между собой и с окружением. Наличие сложного информационного взаимодайствия ые*-ду- задачами в процессе функционирования предъявляет высокие требования к нроцесоу разработки и анализа 'корректности взаимодействия программ в.АСУ.
" Перспективна направлением разработки многозадачного ПО АСУ является разработка взаимодействия программ на основе спецификаций допустимых временных последовательностей.событий взаимодействия. При 'этом конструктивним аппаратом представления и .логіїческо-го анализа спецификаций допустимых последовательностей' событий взаимодействия программ является -аппарат-темпоральной логики
/W-. : '.,' -- ;.'. ' . .' ....;.
Указанные особенности ПО АСУ, с одной стороны, и перспективный подход разработки-взаимодействия программ, о другой стороны, позволяют-сформулировать требования к процессу разработки взаимодействия Программ в АСУ, основным из которых: является обеспечение возможности синтеза автоматных моделей взаимодействия--программ на. основе 'спецификаций допустимых, последовательностей- событий на языке, темпоральной логики.' ; '.- . ..,... -Вопросам. разработки, и анализа 'корректности ПО. на основе
спедаїйиісацяй посвящен ряд работ советских щ зарубежных авторов.
Среда них можно выделить статья и монографии В.Н. Агафонова, '
E.jI. Ющенко, В.Д. Ильина, Э.Х. Гнуту, В.А. Непомнящего, Б. Дис
кова, Ч. Хоара, П. Бахманна, К,Р, Апта, Н. Франкеза, Б. Хэлпврна,
С, Овики, Е.М. Кларка, Е.А. Эмерсона, Л. Лэмлорта, 3. Манны,
А. Днузлі, Е.-Р. Олдерога, В.Р, да Ревера, П. Вблпера и др. Нес
мотря на'значительное число работ, проблема синтеза автоматных,
'цоделей взаимодействия программ в АСУ на основе спецификаций до
пустимых последовательностей событий взаимодействия программ и'
анализа корректности их информационного взаимодействия остается
нерешенной.! -
В связи с этим, исследование и.разработка методов и рредсті взаимодействия программ в АСУ.представляет собой актуальну*) задачу, важную как с научной, так в с практической точек зрения. '.
Цель работы. Основной целью диссертационной работу является исследование и разработка методов ^средств взаимодействия программ в АСУ на основе спецификаций темпоральной"логики, позволяющих сократить затраты на проектирование-и. улучшить качество мне— 'гозадачного ПО АСУ за счет.формализации и автоматизации разработки автоматных моделей взаимодействия программ и'анализа корректности их Мфорыационного взаимодействия. -'.'.
В соответствии с указанной целью в работе поставлены и решены слепувдие задачи. ...;'-'.
Г. Разработка формализма представления и логического анализа спеїщфикавдй допустимых последовательностей событий взаимодействия программ в АСУ на основе аппарата темпоральной логики.
2. Разработка метода синтеза автоматных моделей взаимодейст
вия программ в АСУ на основе спецификаций темпоральной логики с
' применением процедудш анализа: выполнимости формул спецификаций
3, Создание матодаки разработки взаикюдействия. прогр'амі4 и
анализа корректности их информационного взаимодействия на осно
ве ^спецификаций . темпоральной логики , ,
4.^Разработка спецификаций темпоральной'логики взаимодействия процессор системы управления, участком ЩС,, .'''
:5.^Разработка автоматной модели взаимодействия процессов систему управления-участком ГЦС на основе прямененяя .процедуры
строения модельного графа формул спецификаций темпоральной до
ки. .
Методы исследований. При проведении исследований в диссерта-. онной работе использованы"положения и методы классической мате-.тяческой логики, темпоральной логики, теории автоматов, формальне языков, аппарата алгебраических спецификаций, взяимодействую*-х последовательных процессов Ч. Хоара, теоретического программи-івания, теории графов. .
Новые научные результаты. '
1. Формализм представления и логического анализа специфика-
!й допустимых последовательностей событий взаимодействия программ
АСУ на основе аппарата темпоральной логики А. Пнуэли, отличай-.
!йся использованием вложенных темпоральных операторов "пока" и:
: тех пор", позволяющий описать временные свойства взаимодейст-иг программ за счет.семантика темпоральных операторов.:
-
Метод синтеза автоматных моделей взаимодействия программ АСУ на основа спецификация темпоральной логики, отличающийся . строением модельного графа спецификаций на основе процедуры аяа-йа выполнимости; формул темпоральной логики П.Волпера-З.Майны,' заводящий алгоритмизировать синтез автоматных моделей как на зносе спецификаций допустимыхпоследовагел" гостей событий взаамо-эйствия, так. и на основе спецификаций допустимых последователь--эстей состояний взаимодействующих программ за счет однотипности роцедуры анализа выполнимости формул спегификаций временных пос-эдовательноотей на языке темпоральной логики..
-
Методика разработки л анализа корректности взаимодействия рограмм в АСУ, отличающаяся 'формализацией основных .этапов пос-роєния спецификаций и анализа их корректности на основе апнара-а темпоральной логики и. алгебраичєсіда'спецификаций, разработкой втоматной модели взаимодействия программ, позволяющая проектйро-ать логику сшіхронизациЬнкой части програли* за счет построения окальнкх автоматных моделей и уравнений перехода.
.4,- Спецификации взаимодействия процессов системы управления
частком механообработки ГПС на языке темпоральной логики,,от-,
ичающиеся модульностью, полнотой л иолрогкворечивостья описания
опустимых последовательностей событий взаимодействия,' о'беспе- иваю'щйе построение автоматной модели взаимодействия процессор.
за счет применения процедури анализа выполнимости и построения дельного графа формул спецификаций.
5. Глобальная автоматная модель взаимодействия процессов с темы управления участком ГІІС, отличающаяся полнотой множества возможных последовательностей событий взаимодействия, порождаемых моделью, обеспечивающая построение локальных автоматных мод лей за счет процедуры декомпозиции модели-взаимодействия относа тельяо локальных- алфавитов процессов,
'' " Практическая ценность. Практическая ценность результатов р 'бота состоит в следующем.
-
Разработаны инструментальный комплекс автоматизации раз работки спецификаций ИКАРС, позволяющий автоматизировать процес построения спецификаций и их логического анализа, и комплекс ра работки и анализа корректности информационного взаимодействия программ, дозволяющий в интерактивном режиме проводить разработ ку й отладку взаимодействия программ многозадачного ПО АСУ,
-
Разработан пакет программных средств взаимодействия про грамм, предоставляющий разработчикам многозадачного ПО АСУ -йдеш добние'средства взаимодействия программ на языке Паскаль в опер ционной среде ОСРВ 3.1 CM-142Q.
Реадизапия в.промышленности. Исследования и разработки, ви полненные в диссертационной работе, являются частью хоздоговоре них научно-исследовательских работ» проводимых на кафедреАвтом тизироіанвдх систем обработки информации и управления Ленинград ского ордена Ленина и ордена Октябрьской Революции электротехни чёского института имени В.И.Ульянова (Ленина) и использованы в ЛШЮ "Электронмаш" и на электромеханическом заводе "Буревестник г.: Гатчина.' Гарантированный годовой экономический эффект, от использования результатов работы составляет 31 тысячу рублей.
' Апробация работы. Основные положения и.результаты диссёрта ционной работы были изложены и обсуждались-на:
'." - XI Всесоюзном совещании по проблемам управления "Проблем управления- 89"' /Ташкент V 1989/.;
,,:, - Всесоюзном научно-техническом семинаре "Мобильное програ
мное обеспечение" /Калинин, '1S88/;' ...
- Всесоюзной научно-технической конференции "Конструкторе»
эхнологическая информатика, автоматизированное сознание машин и
зхнологий КТИ - 89" /йосква, 1989/; . - . ' . '.
. - Третьем региональном семинаре "Распределенная обработка
нформацйи" /Улан-Удэ, 1980/; ','.
Региональной' научно-технической конференции "Перспективные вправления развития автоматизированных систем управления и их ОМП0Н8НТ0В" /Омск, 1989/;
Республиканской научно-технической конференции "Проблемы втоматйзашш перенастраиваемых производств в машиностроении" "' Волгоград, 1988/; , - .
Научно-технической конференции "Проблемно-методические и ірограммно-тєхнйческие комплексы САПР и АСТШГ /Иаевсй,,1988/; .
Научно-технической конференции "Цифровые методы в решении іапдч управления* /Днепропетровск, 1989/;
Научно-технических конференциях профессорско-преподаватель-!кого: состава ЛЗТИш№ки В.И.Ульянова /Ленина/ в 1987 - :" ' L990 гг. .'"'.
Публикации. По материалам днссертационноЯ работы опубликова-
IO-7 печатных рабої. .' ' .' '
..Структура и. объем работы. Диссертационная работа состоит из-
зведення, четырех глав с выводами, заключе ія, списка литературы
і пяти приложений. Основной текст работы изложен на 149 страни
цах .машинописного текста,, содержат 17 рисунков, 4 таблицы.-Список
/гатературы включает 151 наименование. . '
'\. ' 'КРАТКОЕ СОДЕРЖАНИЕ-РАБОТЫ . -:..;".
Во введении обосновывается актуальность, проблемы^ формула-
руютя цель и.задачи диссертационной работы, приводится ее крат-т
кое содержание^ ' . , :'"''.
ft первой главе ^Рассматриваются особенности автоматизированных систем управления,' дается общая характеристика программного обеспечения "АСУ, характеристика проблемы разработка взаимодействия программ в АСУ, приведен обзор существугадих методов, и средств разработки ПО АСУ»'ставится и формулируется задача.:' разработки взаимодействия программ в АСУ на-основе спецификаций допустимых последовательностей событий взаимодействия
на языке темпоральной логики.
Анализ особенностей АСУ я, в частности, АСУ гибкими произвс ствеиннми системами приводит, к выводу, что цля таких систем харг терна децентрализованная структура управления, доогофункциональ-йость ПО и распределенный характер обработки информации. В силу указанных особенностей ПО таких систем реализуется в виде сово-'купности взаимодействующих процессов /задач/. Наличие сложного информационного взаимодействия между процессами предъявляет особые требования к разработке взаимодействия программ в АСУ.
Под взаимодействием программ понимается взаимодействие программных процессов, т. е. процессов, порождаемых соответствующиг ми программами при их выполнении на ЭВМ. Взаимодействие процессе определяется как событие обмена данн щ между ними, Взаимодейсті процессов может быть реализовано как с помощью механизма приема/ передачи сообщений, так и посредством общей памяти. Взаимодействие с помощью механизма приема/передачи сообщений подразделяете! на синхронное и асинхронное. .:
Разработка взаимодействия программ определяется как процеас проектирования логики взаимодействующих процессов, удовлетворяющей как функциональным спецификациям, так и логическим специфика циям взаимодействия процессов. Предлржено разделение.логики взал недействующих процессов на функциональную логику /логика функцио нальной части процесаов/ и логику взаимодействия /логика синхронизационной части процессов/..
Проведен обзор и сравнительна, анализ, методов и'средств раз
работки программных систем. Выявлено, что. наиболее выразительны
ми и перспективными средствами анализа и разработки взаимодей
ствия процессов являются следующие средства:' -. .." ; .'
-.-расширенные конечные автоматы; *'..', ..'-.'.
.'-' сети Петри; ... ..';"
> ,; - аппарат' С 3 Р взаимодействующих последовательных процессе
Ч. Хоара; . '
.' . -г исчисление СС$ взаимодействующих систем Р.'Мйлнера; ';-, - .темпоральная логика А., Пнуали: ' -. .:' Рассмотрены преимущества и недостатки перечисленных средств из, .которых'следует несовершенство; первых четырех средств, В ' чистом.ви*:9 применительно %. задач разработки взадоодейотвйя .
оцессов и целесообразность использования темпоральной логики в честве формального средства описания л логического анашза взаи-действия. Предложено использовать.сочетаниеразличных формаль- . ос среяств анатаза на разных этапах разработки.. 3 качестве сред-ва'представления логики взаимодействия процессов предложено ис-льэрвать расширенные конечные автоматы, для которых существуют лее.развитые по сравнению с-сетями Петри, способы перехода от. іафкчбского задания логика к программному. G использованием ко-1чных автокатов задача синтеза логики взаимодействия процае'сов"'. юдится к задаче синтеза автоматной модели взаимодействуя гк> ло-[чёским специфйкациягл. В качестве'языка спецификаций взаимоцей-'вия программных процессов предложено использовать формальный ... шарат темпоральной логики, который обладает большей универсаль-ютью по. сравнению с языкгмй CSP и CCS и большими вырази--ільнйми возможностями по сравнения о языком спецификаций логика >едидатов первого порядка.
Во второй главе проводится исследование продуктивних авто- . тих моделей применительно к задаче разработки взаимодействия юграммных процессаа, рассматривается аппарат темпоральной логи-[ в качестве основы формачизыа спецификации взаимодействия про-юсов,', предложены алгоритмы разработки спецификаций взаиічір'цейст'-ія процессов на языке темпоральной логики , алгоритм анализа кор-жтности взаимодействия и метод синтеза автоматных моделей- взаи-ідействия . процессов на основе спецификаций темпоральной.-логи-
Продуктивные;автоматные дадели.являются расширением тради-
юнных автоматных моделей условиями сильной и слабой пролуктив--
юти, при, недетерминированном, вылолкекии переходов автоматов. .-.
«овил продуктивности гарантируют выполнение спемфицяруемых ими.
феходов автоматных моделей прл неоднократной или непрерывной их
(товностй к выполнению..Предложены продуктивные автоматные моде-
I для: а/ взаимодействующих процессов с общей памятью; б/ про-
!ссоб, взаимодействующих с помэщвю механизма-сообщений синхрон-
ы. способом; в/ процессов, взаимодействующих с помощью механизма
юбшений асинхронным способом., - * /,...-
: Программная система Р "-/состоящая из /? взаимодействующих зограмм, представляется совокупностью процессов Pi) (if i'n-),
функционирующих параллельно и взаимодействующих межцу собой и с окружением, т. е.- в виде следующей параллельной композиции:
Р = АІ|рЛєіГ.. . Ця,
где'Л - оператор параллельной композиции.
Выявлено, что такие системы описываются продуктивными автоматник моделями, для них характерно недетерминированное поведение и описание их взаимодействия невозможно только о помощью троек Хоара (я) р {&) , т, е. в терминах предусловий R постусловий 0-.
Поведение программной системы взяимодействущих процессов, заданных продуктивными автоматными моделями, определяется множеі твои допустимых временных последовав льностей событий взаимодей ствия и состояний взаимодействующих процессов. Такие временные последовательности имег вид:
О и-о —* сі і '' « и г " ' ** Ц * —*~-
rite йі - состояние системы, определяемое значениями программны 'переменных; Ті - событие /переход/, переводящее систему из те щего состояния ut в следующее состояние йі+* . При разработ взаимодействия процессов событиями Т* являются события взаим действия, т. е. события приема/передачи сообщений.
В диссертационной работе предлагается использовать аппарат темпоральной логики А. Пнуэли для описания временных послецова тельностей событий и состояний при разработке логических специ$ каодй взаимодействия процессов. В качестве основы языка сиецифи каций предлагается использовать подмножество темпоральной логик а именно, пропозициональную темпоральную логику /ПТЛ/, которая представляет собой расширение традиционной.логики исчисления высказываний темпоральными операторам» будущего и прошедшего вр мени: О - "всегда", О' - "когда-нибудь", О - "следующее U> - "пока", Ы - "оильное пока", Q - "всегда в прошлом Ф - "иногда в 'прошлом"-', 0 - - "предыдущее", 3 - "с тех пор", ,5 - "сильное с тех пор".
Если /< и l/г являются формулами классической, логики, ч Утвержденив о /< будет-истино, если J-4 истина в..текущий мох и во .г.ре моменты времени, посла дующие текущему;-О $* ' истино,
если J\ будет истина в- некоторый момент времени в будущем; Ол иотино, если ' J* истина в следующий момент времени; Л UJz истино, если J а будет истина всегда в будущем или J г. .будет истина в некоторый момент времени в будущем и до этого момента истина ; истино, если существует такой момент времени в будущемt корда Jz истина и до этого момента истина J і Аналогично определяется семантика операторов прошедшего времени относительно времени в прошлом.
Исследованы-выразительные^свойства формул ПТЛ. Проведена классификация, свойств,, выразимых формулами ПТЛ.' На основе выражения канонического разложения формул темпоральной логики,
хм \ OoSi VOQ d~i),.
выделены возможные подформулы, которым соответствуют следующие свойства: uS - "безопасность", 0 - "живучесть", p/v О ot -"альтернативность", fo [aJi v о cLl) - "глобальная альтернативность", DO/ - "отзывчивость", Ouj - "настойчи-вость", рч>У v OQcL - "развйваемоеть",ЯГ«(0-^ voootij "глобальная развиваемое!*", где. Ji± dt^i^tjA*) - формулы темпоральной логики прошедшего времени.
Для представления произвольных временных последовательностей
с фиксированным порядком следования событий, предложены специаль
ные конструкции вложенных темпоральных операторов "пока" и
"с тех' пор"': .»:'.
семантика которых определяет следующий временной порядок истинности, формул Л,/»,.-'., J* относительно будущего времени, в первом случае и относительно прошедшего - во втором: если-в некоторый момент времени истина формула -^» , в следующий момент истина некоторая формула Jj , где І j 4 >*
Рассмотрены алгоритмы разработки спецификаций в рамках формализма ПТЛ для конкретных примеров взаимодействия процессов.
Предложен алгоритм анализа корректности ззаимоцойствующих процессов на основе развития метода индуктивных утверждений
Р. Флойда и аксиоматического метода Ч. Хоара на случай задания логики процессов продуктивными автоматными моделями, позволяющий проводить анализ частичной корректности взаимодействующих процессов на ранних этапах разработки до написания кода. .
Алгоритм отличается:
а/ особыми спецификациями процессов видаїш"^(vj , для которых в отличие от традиционных троек Хоара не требуется знание программной логики специфицируемого процесса Р и семййтика которых определяется импликациями вида:
[^ (а) ~ а! є «г (а)) —' wa'j,
где С - переход процесса Р ; ,
б/ правилом инварианта для доказательства свойств корректности
н- Я — f .
. #- fflTif}
н- a .'
где Т — множество всевозможных переходов процесса Р у определяемое на основе продуктивной'автоматной модели; Ц -предусловие процесса.
В диссертационной работе предлагается метод синтеза автома ных моделей взаимодействия процессов на основе спецификаций на языке ПТЛ, который отличается от-известных метоцов Е.М. Кларка-Е.А. Эмерсона, П. Волпера - 3. Канны, Е.-Р. Олдерога тем, что позволяет синтезировать автоматные модели взаимодействия'какда .основе спецификаций ' допустимых последовательностей событий,взал-мо действия, так и на основе спецификаций -допустимых последовательностей состояний процессов. В основу метода положена процедура анализа выполнимости формул ПТЛ, основанная на декомпозтии формул ПТЛ на формулы текущего'состояния /формулы классической /логики-/ и формулы следующего состояния '/формулы ПТЛ, -прёдва- ' ренине оператором, О /. :,;.',
:: ^ .Процедура декомпозиции и анализа выполнимости формул ПТЛ используется, для построения модельного графа формул спецкфикациі
Модельный граф является графическим воплощением всех моделей формул спецификаций на языке ПТЛ, т. е. является порождающим автоматом всех допустимых временных последовательностей, удовлетворяющих формулам спецификаций.
Исходными данными для процедуры декомпозиции и анализа выполнимости является исходное множество формул "21 и некоторая логическая переменная спецификаций ^. , значение которой принимается истинным. Результатом выполнения процедуры является множество 2T«j подмножеств z"^ формул темпоральной логики, т. е. ^«гЙ^V-Z^-Z/i/} . i,je{Oj ,.--3 , где J-ij - формула спецификаций. Множества г' состоят из формул следующего состояния.
Процедура построения модельного графа состоит в выполнении следующих шагов:
-
Построить граф, состоящий из одного единственного узла, помеченного исходным множеством формул спецификаций 2"
-
Повторить шаг 3 для всех узлов графа.
-
Для каждой логической переменной q формул спецификаций выполнить:
а/ применить процедуру декомпозиции множества формул рассматриваемого узла при'-истинном значении ty . ;
б/ для каждого подмножества z множества ^ц. , полученного в результате применения процедуры декомпозиции, создать лугу, помеченную множеством форвдул /$} U 2Г^ f с началом в . текущем узле и концом в .узле, помеченном множеством форлул г-! ; если таких узлов нет создать новый.
- При-построении модельного графа формул спецификаций взаимодействия процессов строится граф, который интерпретируется в качестве, конечно-автоматной модели взаимодействия процессов.
Третья глава посвящена разработке функциональных .спецификаций программного обеспечения система управления участком механообработки ГПС на языке описания графо-иерархичёских структур, .логических спецификаций взаимодействия процессов программного обеспечения'системы управления участком на языке темпоральной логики, глобальной автоматной модели протокола взаимодействия процессов системы управления на основе спецификаций темпоральной
логики в соответствии с методом синтеза автоматных моделей взаимодействия процессов; декомпозиции глобальной автоматной модели и построению локальных автоматных моделей процессов системы управления.
Программное обеспечение системы управления участком представляется совокупностью программных модулей, реализованных в виде взаимодейству здкх программных процессов.
Процесс проектирования ПО системы вз'аимодействующих*про-цессов системы управления участком представлен в виде двух . взаимосвязанных этапов:
а/ проектирование функциональной части процессов на основе функциональных спецификаций;
.6/ проектирование синхронизационной части процессов /логики взаимодействия/ на основе логических спецификаций взаимодействия.
Разработаны логические спецификации взаимодействия процессов
системы управления участком.Б процессе взаимодействия один процее
выступает в роли главного, другой-в роли подчиненного. Обозначим
их соответственно 17 и ПУ. В качестве элементарных действий
взаимодействия главного и.подчиненного процессов выбраны следую
щие действия: ПОСЛАТЬ_ГУ, ГОСЛАГЬПУ, ПРИНЯТЬ_Г7, .'ПРШЯТЬ_ДУ,
т. е. действия передачи и приема сообщений'соответственно глав
ным и подчиненным процессами. Спецификации взаимодействия процес
сов ГУ. и Ш составлены в терминах следующих событий готовности .
выполнения действия взаимодействия: послать_ГУ, послать_ПУ,
принять_ГУ, пршять_П7. _;'
.. Получены следующие^обобщенные спецификации взаимодействия
процессов ГУ и ПУ на языке ПТЛ: "
Т процесс_ГУ U-послать_ГУ; ' ' D /принять_ГУ -~ 0/~\ процесс_ГУ U послать_ГУ//; '
Тпроцесс_ПУ U послать_ПУ;' -'/ D /прлнять_ПУ -»- 0/-)процесс_ПУ V послать^ПУ//;. ;а/поолать_ГУ -* 0/1принять_ГУ V пэслать_ПУ//; ;.' -;, D /послать_ПУ -*- о /~\ принять_ПУ и послать„ГУ//У'. Ь ф /процесс_ГУ/; D О /процесс_ПУ/; .''
.-- 13 -
О/послать_ПУ-«. о / т послать_іи//; о/послать_ГУ- о/ппослать_ГУ//; d /послать_1У - О /послать_ПУ V ~\ послать_ГУ//; а/послать_ПУ — о /послать_ГУ V -] послать_ПУ//; \'лроцесс_ГУ = поолать_ГУ V принять_ГУ; процесс_ПУ = послать_ПУ У принять_ПУ.
Разработанные. спецификации отличаются модульностью, полнотой и непротиворечивостью описания допустимых послецовательнос-- гей событий взаимодействия процессов программного обеспечения системы управления участком и позволяет строить глобальную автоматную модель взаимодействия за счет, применения метода синтеза автоматных моделей взаимодействия на основе спецификаций темпоральной логики.
На основе полученных спецификаций темпоральной логики построена глобальная автоматная модель взаимодействия. Модель отличается полнотой множества всевозможных последовательностей событий взаимодействия, порождаемых моцелью,и обеспечивает построение локальных автоматных моделей процессов за счет применения процедуры декомпозиции, глобальной модели относительно локальных алфавитов событий взаимодействия процессов. -
Локальные автоматные модели используются'для разработки логики оинхронизационной части процессов посредством инвертирования и составления уравнений переходов в "соответствии с предложенной методикой разработки взаимодействия программ.
Четвертая глава посвяцеяа разработке инструментального и методического обеспечения процесса разработки спецификаций, проектирования и отладки, взаимодействия процессов ПО 'АСУ.
Реализован инструментальный комплекс автоматизации разработки " ' функциональных спецификаций ИКАРС для автоматизированной поддержки, процесса построения спецификаций п их логического анатаза' на основе совокупности взаимосвязанных моделей представления, проектов ПО АСУ: функциональная модель, модель данных, модель логики модулей, модель структуры модулей. .'. Описан комплеко разработки" и анализа корректности информационного взаимодействия процессов ПО АСУ, взаимодействующих
на основе механизма приема/передачи сообщений, позволяющий проводить, разработку и отладку в интерактивном режиме взаимодействия програмних процессов многозадачного ПО АСУ, а также исследовать и протоколировать фактические последовательности сообщений взаимодействия в специальный файл отчетов доя последующего их анализа средствами инструментального комплекса ЖАРС.
Разработан пакет программных средств взаимодействия прогоамм предоставляющий разработчикам многозадачного ПО АСУ адапэдобные средства взаимодействие программ на языке Паскаль*
Предложенные средства разработаны на языке Паскаль в операционной среде ОСРВ 3.1 СЫ-1420,
Предложена методика разработки и анализа корректности взаимо
действия программ в.АСУ, отличающаяся формализацией ' основных
этапов Гйостроения спецификаций и анализа их корректности на
основе-аппарата темпоральной логики и алгебраических специфика
ций, разработкой автоматной модели взаимодействия программ, поз
воляющая' проектировать логику синхронизационной части программ
за счет построения локальных автоматных моделей и уравнений пе
реходов. ,-.''-.'
Проведено.экспериментальное исследование предложенных средств и анализ их оф$ективности согласно методики. ГОСТ 28195-89 "Оценка качества программных средств" . Анализ показал целесообразность использования предложенных средств в качестве инструментального и методического обеспечения процесса разработки . взаимодействия програлзл в АСУ.
