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

РГВ од

На правах рукописи МАТЮНИНА Ольга Евгеньевна

УДК 622.3:658.512.011.56

ЛОГИЧЕСКИЕ МЕТОДЫ И ИНСТРУМЕНТАЛЬНЫЕ СРЕДСТВА ВЕРИФИКАЦИИ ОФИСНЫХ ПРОЦЕДУР

Специальность 05.13.12 — «Системы автоматизации проектирования (промышленность)»

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

кандидата технических наук

Москва 1995

Работа выполнена в Московском государственном горном университете.

Научный руководитель докт. техн. наук, проф. РЯК.ИН О. М.

Официальные оппоненты: акад., докт. техн. наук, проф. МОСКАТОВ Г. К. канд. техн. паук, доц. ХОРЕВ П. Б.

Ведущая организация — Всероссийский НИИ проблем вычислительной техники и информатики Комитета при Президенте Российской Федерации по политике информатизации.

Защита диссертации состоится « /Ф. » 1995 г.

в /г. час. б'иа заседании диссертационного совета Д-053.12.12 в Московском государственном горном университете по адресу: 117935, Москва, В-49, Ленинский проспект, 6.

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

Автореферат разослан « , » у^^. . . 199-Г"г.

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

канд. техн. наук, доц. РЕДКОЗУБОВ М. А.

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

Йцтуалкиость работы. Автоматизация o-»Mcai (jff ice autd««t ion) — одно и9 вакнойпин направлений испдпьаоелния ПЭВМ, л>па>> пансипальный эфф»-<т сропи возможный приложений КОКПЬМТвгрОВ. Это н41г1рд)9п ении, не сухи, продолжило ранее суцвствоаавнсв пйпупярнои направпвниа — АСУ» Основное отличие« кпассимчск»! идеологии АСУ — аатоиатиааиия "сверку-вми з ", в то ерет» нак о#исные системы — автонатнэамил "сии я у—я»ерк " от источников и потребителей информации. Это чеаовеь»-нааниные систены распределенного упраапения, обычно >- е имеюяие "кестного" центра.

Кпичепое понятие офисным систем — яонумимг. СисК'Ич — сеть иа разного пила ресурсов <ЗВМ, человен -агент, ионнуникации, срелстаа ияперенив, автоматы и др, ), взаимодействующим для выполнения поставленным задлч. Как аапачи, там и сама система могут иененяться (»волиционироватк) в процессе »униционироаания. Реааепыв «адачи свяеанм с обработкой, приемом, передачей, хранением, размножением, создание» документов. В системе суяестиенна pont» челоэена и бумажные документы обычно сосуществуют с мамнннипи документами. 0*исное действие — ото любое действие » о*исв, такое, как редактирование тенета, обраюваии» •ори, поиск информации, отправление и прием сообщений, принятие ревемий и др.

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

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

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

Наименее исследованной является проблема верификации, которой посаяаена данная работа.

Верификация — проверка соответствия проекта системным требованпян по *ункцнонирав*нип офисной сметены.

В>риаик>ии<1 май один из важным этапов •автоматизированного проектирования офисным систем позволяет оценить корректность проекта до его Фактического воплощения (реализации), получив танин образом существенную экономию ресурсов по сравнению с оиенкой качества на реализованным проектам. Эта ОМОМО0ИЯ тем выяг, чем спожмее ' истема и дороже ее материальная база. ?

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

В данной работе решаются следующие задачиi

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

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

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

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

5. Разработка инструментальных средств поддержим язына спецификации и процессов верификации офисным'процедур для разработанным методов. *

Научная новизна работы заключается в разработке* - логического языка спецификации офисных процедур)

- 1 -i—

— п»годов проектирования информационно—логической полепи имений процедуры с принен»ниеп СЙЗЕ-текнопогии 5

— погиуесннк методов верификации о*иснык процедур.

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

Реализация работы. Разработанные имструнентлпьныв средства и потони автоматизированного проектирования о*иснык процедур внедрены при автоматизированном проектировании передвижного комплекса для подготовим к обогащению алмазосодержащих глинистым песков месторождения "Горнов" Мириенского ГОКа акционерной иомпаним "йппазы РОССИИ-СЙХЙ", а также к учебном процессе при нурсовоп и дипломном проектировании систем управления в МГГУ и Севаро-Каакаэсион горнометаллургическом институте.

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

апробация' работы. Свержение и основные результаты работы доложены и обсуждены на Всемирном конгрессе 1ТЗ-92 "Информационны» коммуникаций, сети, системы и технологии" «гз-га ноября 1992 г, Москва), на Всемирном конгрессе 1ТБ-93 "Информационные коммуникации, сети, системы и технологии" <25-26 ноября 1993 г., Москва) и на Международной научна—технической конференции "Развитие и применение открытым систем" <12-17 сентября »994 г., Казань).

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

Объем и структура диссертации. Диссертационная работа состоит из введения, четырех глав и заключения.

-з -

с од»? ржт 1£0 сгрлииц машинописного текста, & таблиц, 22 риоунна, список пигвратуры из 81 наин*новаииЙ, 2

(¡(i i-i пс

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

Í) Н#СГ ОИЩее пр«ия появпп ется ее* бопьи» новых и спожмми ин^ормац^о^нын т»мнологий, которые находит cao« прим«?н€?м*» в офисных ин*орнамионнык системах. fib'-üiiae^artUHfl офисной работы становится одной ив п if релен гипнын проблем для любых органиааиий. В , и)(.п№Ане* время для »»«»итивного проектирования и амалиоа офисных'нн»орнационных систем 6мл предложен ряд полелей и языков сп«ци*ииаций офисным процедур, вместе с- tím об1ц<мп н етодопогия ' проектирования попу чипа е«е нс.цост« точно €• развитие. Существует необ к о дин ость соалаими сиспенатичесних ивтодопогий, которые о6сс|1*чйи«»вт руководство работой р*иснык аиапитинов и г)о г»оль ин Форпапьныпи инструментами и лравйпами для ноаипо«»йстния с пользователями и для проведения процесса проектирования.

Большинство моделей* которые используются для гимй1)р«ни проекта й сл*ии»нмации офисной ин^орнаиионной системы, су«|«стеук»т независимо от возможных инструментальных особенностей, так мак кодепи стро гея на ионцептуальнон уровне. Моделирование всем аспектов очмисной работы очень затруднено на—аа сложности офисных алйсгиии« состоя«им обычно иа многих номпоиентов,, £ которые пе могут полностью идентифицироваться или ■ьорнапиэоватьсн, Поэтому особенности традиционных концептуальных моделей для информационных систем не йостаточн«, и ОФисиые информационные системы требуют особых моделей и подходов.

Большая роль & автоматизации проектирования офисных систем принадлежит логическим методам. Концепции погического подхода х информационным технологиях были созданы трудами многих учень.х о области информатики В. М. Г^ушноеа, М.А*Раврипова, В.А.Горбатова, Я.А.Поспелова и др.

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

-к-

ученые Д. П.Ершов, С.С.Лавров, Я.М.Барзяннь, , А.й,Стогний, Е. Л. Ющенко, С. А. Юдицкий и др.

Современная «»тодопогия проектирования о»ис«ык систем""включает разработку спецификации, пояепиро»««ис системы (посредством испопниных спецификаций) и аври*икаиии системы.

Верификация - проверна соответствия проекта системным требованиям по Функционированию офисной системы. Проверка может охватывать» явно

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

Ранее проблема верификации была исследована применительно к программам на языках высокого уровня (Паскаль, ПЛ/1, Модула-г и др.) и разработан ряд Эффективных методов верифинации программ (доказательства корректности программ).

В создании логическим методов верификации программ больаой вклад внесли от|' юстэеиные и зарубежные ученые» й.П.Ервов, Д. й. Яетичевсмий, В.Й.Непомнящий, О.М.Рякин, Н.Вирт, Э.Деймстра, Д.Грис, З.Канна, Д.Лаймам, Ч.Хоар, Р.Флойд.

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

Дрмитектуры офисных информационным систем яципшо рассматриваются в питературе. Сыпи предложены отлальны»

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

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

Для успешного применения новым темнологий в автоматизации ОФИса необходимо четно понимать организацию офисной работы. В последнее время в научно-исследовательской литературе для эффективного проектирования и анализа офисным информационных систем был предложен ряд моделей м языков спецификаций офисных процедур. Эти модели расамрипи традиционные подходы к им-орпационнып системам и базам данным путем оБк.едннен'ия новый особенностей офисным информационных систем. В частности, алененты данным обогащены объединением неструктурированных данным и новыми типами данным (документы, досье); сделан акцент на динамическом описании офисной среды, т.е. передачи информации и управления о офисным процедурах.

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

Подели баз данным. В этик моделях основное внимание обращено на данные. Базисные элементы этого типа моделей — это типовые данные и данные манипуляции операторов (сохранение, восстановление, манипуляция, neptfy4al. Все Офисные действия модепируются^как операции на данным. Обычно, данные представляются в виде Форм, которые сходны для бумажным Форм в традиционным Офисам.

'б"

а. ПроцеЬсно— ориентированные« нодепи. Эти полепи исполыупт соответствующйе элементы действий, истории-выполняются соответствующими офисными работникапи (или агентами). Основная цель модели — это описать управлнпаий поток "в рамкак офисной работы с поиоцыо правил, которые должны удовлетворять офиснык дейстоипч.

3. Смешанная модель. Зги модели не делают акцента на элементам данным ипи процесса, но используют им о&<>. Большинство современный офисным моделей принадлежит к сиеванной категории, так ман они допускают Более полную спецификацию элементов Ja оаисе и их взаимосвязи (внутренние связности).

Далее в работе разработан r>uk спецификации олиснык процедур, сочетающий средства методологии проектирования OSIRIS и СЙВЕ-тек нологии, базирующейся на инструментальной системе CASE-Оналитик, в результате чего обеспечена возможность автоматизированного проектирования спецификаций офисным процедур, интеграции офисным процедур в систему и графического представления спецификаций.

Язык спецификации офисным процедур.

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

Структурные элементы модели!

— документы — это собрание элементарных данным.(Типы элементарным данным! структурные поля, свободный текст, сообщения, изображения и т.д.>|

— досье - это собрание документов.(Документы группируются в пределам досье по содержанию или по структуре);

— агенты представлены отдельными служащими, группами или категориями служащим|

— действия представляют в подели работу Офиса.

Спецификация документов, . досье, агентов, действий использует иерармии абстракций е Форме совокупности, ассоциации и обобщения. Иерархия абстракций — это возможность определения элементов модели в'терминам монлонентов уровней. Совокупность лает возможность, учитывая снижение уровней элементов, уникально собрать элементы вместе. Ассоциация позволяет создать Формы относительно высокого уровня элепентов| набор отдельным однородным элементов.

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

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

QSIFilS включает элементы семантической офисной системы (BOS - Semantic office systea) нодели и инФо^ацианнмк управляющим сетс^'. < ICN — Information Control Nets), интегрируя моделирующие черты обоим.

• Ссыпаясь на эту модель, Формализм, который позволяет ныразить синкронизацию операций в линейной •ори», — ото строчные выражения; возможный комплект коннекторов операций)

логледовательность. Операции перечисляются в ток породи«, т которой они должны выполняться.

"|е>" выбор (XOR). Выбор из комплента операций лозволяет проиоойти только одному действию. Селекционное условие "с" всегда ассоциируется с ей 'юроп.

"+с повторение. Повторение^ позволяет произвести операцию несколько раз а зависимости от условия с.

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

"<"")" круглые скобки используются, чтобы сгруппировать операции в более сложные блоки.

Выражение, представляющее операции в процедуре, записывается в соответствии со следующими синтаксическими правилами: S—> ft

й—) ft" J "Й й"|„"й й"4-с"

ЙСТ1VITY-NflME

- & '

Гра*ич*сни* символы языка спецификации

0 действие

о док умеит

о досье

о-о. Предшествование «»жду действия**

о—•□ Со»д«ние дои унейта

0- - - □ Модификаций доцунент*

□—О Дветруи тивиое ислыгдниг эпвмвнта

0--0 Извлечение ин^орнации н.» до купеит*

XOR - соединение! действие 3 может н«ступить, могла либо 1-е, пмбо 3-е действие аавераено. XOR- соединение соответствует соединении двум альтернативным путей в потокоео.н графе

XQR - расцепление) когда действие 1-е »акончено, альтернативно выполняется пиЬо 2-е, либо 3-е действие. XOR -- расяепленне соответствует соэданин двук альтернативным путей в гра*е

AND ~ соединение« действие 3 иомет начинаться только тогда когда и 1-е, и 2-е заверяемы

Л AND - расцепление■ когда действие 1-е закончено, 2-е и 3-е действия ногут начаться

Инаорпационно-пагичасмал модель системы — ото иараркил диаграмм, структурогракм и раалинного рода описаний. Уровни иерархии модели — ото уровни

детализации.

Дпм нормальной записи определении информационно— погич»е«ой попоим исно г! 1. а у «м ногаиим Бокуса—Наура, пшюлнеииул пиража<ниеп для оалнси конструкции

"д»г»ли1яцип".

И«>ра,рмия детализации! 1Ин«ирпл|ионно-погич»си»я нопапь)-)(Контекстная

диаграмма)

(Подсистема)—)(Диаграмма информационным лотокоп) (Управляющий процесс)—) (Диаграмма перекода состояний) |

(Таблица событие—отклик) (Процесс)-)(Диаграмма потоков

данный)|(Миниспецификация) (Потоу. данным)—)(СтруАтурогранмл данным) (Поток управления) -> (СтруктурогррммЬ событий) (Макопитепь данным)—)(Структурограмма накопителя)

•Компоненты модели■

(Контекстная диаграмма) •>< (подскстепа) )

( (внешняя сущность) > {(информационный канал)) <(информационный потом)> (Подсистем*!»(иоиар)(имя)(поставщик) (Внешняя сущность) •» (имя) С (номер копии) 3 (Информационный канал)«■(имя)С(номер копии)3 (Информационный лотом)'(поток данным)I(поток

управления)

(Поток данным)«(имя)

(Диаграмма информационным потонов)ф (контекстная

диаграмма)I (диаграмма потоком управлении)| (диаграмма потоков данным) (Диаграмма потоков управления)ф<(управляющий процесс)>

<(процесс)>

< (информационный канал) > <(внешняя сущность)>

< (поток управлении) > (Управляющий процесс) *» (номер)(имя)

(Процесс:) « (номер) (имя) (реализация) (Диаграниа потоков данным)»((процесс)>

<(управляющий процесс)>

< (внешняя сущность) >

С (информационный канал) >

< (накопитель данным)? ( (лоток данным) >

' (Информационный канал)»(номер ИК> (имя)

С(номер копии)3

(Номер ИК)ф"ИК"(целое)

(Накопитель данным) (номер накопителя) (имя)

С(номер копии)3 (Номер)"(целое не О)"С(номер)1 (Имя) « (буква) С (буква) | (ци«ра)'' "> (Номар копии)ф(целое)1 (Номер накопителя )■* "О" (целое )

- Ю-

Гра*ичесная мотании

Внешняя суя^ссть О

Смст»яы/подсисг»кы Поп» номера —— Попе имени — Попе имени - проектированка :—

Проиесс ропш номера —-— Папе имени - Поп» аичесиой — ре*пиш»ции --

Упраелягаций процесс /• " n Пеле инени —-——( )

Неиолитепн ланник

03

Информационный кднвп Номер и«н«па Попе имени Номер «цпим 1_*|ике , |<—1

Информационный потом -----------' ■> Погон денным

В проектировании »«иоиой информационной системы рашпнчаится ч«гыр( асна^иые •<№! пр<лхрит<П4>ний <и*пи>| аналиа требований, спецификация требования и инструментарий.

Проектирование офиснын процедур р«»6ип»»тся на Е столии1

— проектирование индивидуальный процедур»

— интеграция процедур.

Рааработна сп«чи*ии>цип ,в«исиии процедур н1чмн»»тсп с определения методологического критерии, который яопявн испопкаовдться а иод« проектирования. 1. Одна и таке полет» нелолмауется нан ипв анапиаа, -тли и для спецификации требований.

-

2, Монет, действует нам руководство для проведения офисного анализ« и способствует предотвращению ошибок.

3. Проект должен быть представлен на должном уровне компетентности.

*». В исполнении проекта должна использоваться нисходящая детализация.

5. Анализ исключений в работ», анализ нормального режима работы Офиса.

Б. Проектировщику предоставляется свобода в организации своей«работы. •

7. Необходимы непротиворечивости и законченность ноне.чного требования.

Принер офисной процедуры анализа проб горной породы«

Процедура осуществляется следующим образом. Инженер берет 'пробу горной породы и передает ее (с координатами и датой проьы) в лабораторию онслресс—анализа. Затем лаборант выполняет экспресс-анализ на всенощную полезность пробы. Геолог принимает решение о пробе! отклонить или передать ее на дальнейший (углубленный) анллиа, затем оценивает результат углубленного анализа. Инженер, -ведущий базу данным о пробах, заносит в базу данных результат пробы при отрицательном решении или положительном решении поспв углубленного анализа. Диспетчер Формирует, графин взятия новым проб и др .'их работ.

Огчмни» после проектирования на уровне высшего руководства

N Название Описание

1. г. 3. 5. Взятие пробы Выполнение эиспресс-анализа Решение Занесение результата е базу данным Формирование графика Взятие пробы и передана ее <с координатами и датой) в лабораторию экспресс-анализа Выпопнение эиспресс~аналиэа на воаиожную полезность» пробы Решение о пробе! отклонить или передать на дальнейший (углубленный) анализ и оиениа углубленного анализа Занесение в базу данным результата пробы при отрии. тельноп реяении или положительной режении после уггту&пеимого анализа Форсированна гра+ииа взятия новым проб и других работ

Взятие пробы

Экспресс-* и an и:*

Отрмцат. результат

. ХОЯ

?ние зт/ р

Замесе» отрицат/результата в базу I

Занп»чит»льное состояние

Подготовка

отрицат.

результата

Формирование/ гра« *ма работ

Дополнительный IAND анализ

ПолоЪт овна '"попечительного ответа

Положительный результат

Занесение положит, результата в базу данным

тттгтпт.

Рис.1 Шаги процедуры "Риалиэ_пробы".

■ Методика в«ри*икации офисных процедур

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

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

Игнопии*'СОСТвННИ« - ото «с» опенеиты, моторы« су»<»м»у»1 oV"« «пуск» операции. Состояние шнод« после исполнения сшер«ции - ото состояние, которое СЛ.|Мб«7Н«йЯС11, мочимая с исходного состояния,

(,'нйтримаи успоеип анода и еымода операции.следуюним о fi ц м н о м к

- ,<fcе ялепеиты, предвествуюмие операции и не упомянутые i» условии вход* олграции, суаестаумт в состоянии выкода о п #рации|

- »•<.•» ЗПИ1ГНП1, упомянутые в условии внода и не упонмнуТыг в условии выхода, Дольве не сунествуюг в коми* операции.

Ь«ри*мнаиия рассищ ривается как «орпалыюе

доказательство, которое, при данном верном немодном

ciicTimiw«, соемает вымоднов состояние в соответствии с

• орн«пьнынн пряампл**» логнни операции.

Правима определяются в классической *орпе правил

»иксп«, но с испольаованиеи троен Хоара (I)0<Q>, где

tlMHCn означает, что "если X удовлетворяет немодному

01Ч««и»и по выполнения операции Я и, если выполнен*»

»«н*ич»м«тс», тогда выходное состояние" удовлетворяет Q

<лсч'л* выполнения Й>."

Рассмагриваемый при вери*ин«ции основной набор

логическим правил имеет вид|

I. Пр.реило последовательности. Для

последовательности двух операций А и В имеет место!

jtliOíÓaJ.tlbJBÍCn^Oa э 1Ь

<J>0|BÍQ>

То есть вынодное состояние Оа операции Я долимо

определять анодное условие следующей операции В.

Правило логическим аагов (правило секвенции!.

Это правило косвенно относится к испольауеиоиу яеыну,

но полагает ю поиске домааатепьств!

1э1а,<1а)й<Оа>, OaJO .

С1>й<а>

3. Правило выбора. Операция <Д|„В> выполнена, если операция й, «пи операция О выполнена, что соответствует правилу i

< Ic/\ cWDa), < le /\с)В<аь> < Ic Л с>й|„в<аа 7\оь>

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

По окончании (Й|«В) тольио . алепанты, ибнсп^чшиыи обеими операциями О и В, могут считаться сушсгвуииит! на выходной стадии.

А. Правило параллелизма

{ 1 >й< Оа>, ( 1 МНОЮ < I )й«ГКОа А ПЬ » Оно оанйчавт, что когда две опарацик Н и В оцуяаствлинтс'п параллельно (ЙДО), то истинны соинясткия суждения от рееультатоп обеих операций.

Правило повторения (итерации)I

II/ с)А(Оа>, Оа? О ' I Л.с >й+„<а> Учитывается, что операция О, проповеданная по няныиеА мере один ран, помет быть повторена иеопределенное количества раз. Аля аышщнвнип операции й нужно выпапышнч» условия С, которое проверяется ори каждом повторении.

€>. Правила абстрагирования, йбстракции прис-утстау>от в модели для того, чтобы поаволи!* увеличить уровень описания операций.

Два прлянпт управления абетранкияпиI ^ II - ото 1,<1>А<0> (11>Й<0> <1)0(0),О - »то 01 (1>Й<С»1>

Эти правила выражают следующую концепцию! абстракция - »то импликация, т.е. 0»01, поатоиу может быть применено правило секвенции . Аналогичное обоснование применимо для

Пример верификации офисной процедуры. В качестве примера рассмотрим верижикацию офисной процедуры аналиеа проб горной породы.

Во рм«*и* аиия стадий процедуры "Анвлиэ__про6ы". Операция

Иенояное попечение

входные условия

Выи одные условия

Бык едное поможеиие

инженер! А лаборант/ геолог/ инженерё?Л диспетчер

«)Клптие

п(<обы

про Ьа / инженер!

проба координаты/\ координаты/ дата_пробы дата_пробы инженер!

I.'? Эк спресс^.

и оординатыА яаборантл оиенка^пробы дага.пробы/^ ноординатыД инженер! дагапробы

результат _анали за Л геопог

с > йопопни-п?пьм«й _ анализ

«1) ПОДГ'ОТ .

лапомит.

от8»т|

результа т»__ анализ а А

геолог

результат^ оценна_

анализа/ угпубпенного_ углуЬпёнмого.. геолог анализа анализа/

геолог

оценка_ . о цени а__ создание^ создание_

у г лу 6 л<Г и ного^ углубпенного_ базы " б а э ы _

анализа/ аналиэаА данным/% данник Д

геолог геолог инженер«? инженере?

^ ) Занесение _ создание_ с издание _ занп»«чит._ аакпючит. _

результата^" базы _/*анмымЛбаэы_данныкА состояние состояние и б<иу я^ннык инженерЗ инженере? '

1)Форниро-вание гра#ии а__ р а б о т

оценка_ углублен, анализа/ геолог

яиспвтнерА дага_лробы

•ориироеание

гра*ина_

работ

Формирование _ графика __ .работ

д)Подго- оиенка_ отрииат»_ тояка стриил- углубл. __ результат^,

тельного. анапи зад анапиэаД

результата геолог инженера

отрицатепьио#_ эанесение_ реаение отрии._

ре эультата__ в_баэу_даниык

Ь)Занесение оуенма_ * результата углублен. _ • _Ы»у_д»инык а на пи за д"* инженере"

ре эультат_ анализа А инженере?

заключит. состояние"

заключит, состояние

•ориироваиие_баэы_даннык

*|Ь|(<д;Ь>|(с«(<с1«»>&Г)))

Немодное состояние* инжеиер1 Апаборант/ геолог/

4 рнжеиер2 ддиспетчер

Вмиодное состояние» жорпировани»_6«аыданный

Проведем а»ри*ииацим этой офисной процедуры. Согласно правилу последовательности для операций и Ь, при исходной ситуации з проба Дини<енер1

Так как СЗа^выходное состояние Вэятие_пробы""

' координаты / дата_пробы А инженер1 и входное успоаик

операции Экспр«сс_дналиом координаты Д дата__пробы Д инженер1, (ЗаЭ1Ь, т.е. спецификация верна.

Далее следует операция отбора (g)|(ct<(dfе)&f>). Рассмотрим | <ct<<díe)Af>>>.

Исходное состояние« ин*ен»р1Л лаборант^ геолог/ инкенерЗ Л диспетчер.

Выгодное состояние« форнировамие_6аоы_яанных.

Исходное состояние« 1«реэультат_анализа Л геолог.

Входное условие для < g | h ) I оценка_углубленного_аналиэаА инженер2.

Входное условие для < с | ( <d | е> %f) ) i р«»/льтат_аналии геолог.

Выходное состояние для (g|h)t эанесенме_отрицатепьного реаультата_в_баэуданных Л заключительно« ^состояние. Выходное состояние для <с|<<d|е>if))t оценка_углу б ленного_ анализа геолог^

coaдание_базы^данных Линженер2 Д •»ориирование_ графика — работ.

Выходное состояние« Форнирование_баэы_данных.

Таким образом«

íc* геолог.

С" результат_аналиэа.

Итан

1Э I I в

I t >

Q<Bih» /v Q . ■ , < <«»,«> a > > Формирование_базы _яанныи) Q. Рассмотрим параллельные операции <<d|e>Af>

с исходным условием« оценка_углубленного_аналиэаИ

геолог.

заключительное^состояние.

О Формирование_графика_работ.

Получается

/I О," заключительное_состояние

ФОрмирование_граФика_рлйот.

В работе разработана нетодика логической спецификации офисных процедур и их интеграции дпя

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

Рис.г Ииепркаиионно-логическая модель офисной процедуры "Анализ проб горной породы"

Инструментальные средства верифииации офиснык процедур

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

В основе идеологии инструментальным средств лежит СЙБЕ-темнология. В разработанно- инструментарии также нашли свое применение подкопы н моделированию офисным процедур и ОБ1Р1Б-нетодология проектирования офиснык систем.

чв-

Система выполняет спедуюмив Функции:

— создание информационно—логических моделей)

— создание базы данный модели;

— редактирование моделей из базы данных;

— помочь польз о вате л к»;

— вериФимациц созданных моделей.

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

Система использует спедумщий набор графических элементов ж

1) Внешние сущности. 2> Системы/подсистемы. 3>* Процесс.

А) Управляющий процесс. 5> Накопители данных.

6) Информационный канал,

7) Информационный поток.

Основные характеристики инструментария

Объем ПО Загрузочный модуль 1 40 иБ <поридна 1 ООО строк исходного текста)

Среда MS-DOS версия 5 - *

Ограничения на ПЭВМ ПЭВМ типа PC 28€>. 306* с объемом дисковой паняти не менее нО М1э. оперативной памяти 6АО кБ

Временные карайтеристин и Затраты времени л . создание одной информационно*- логической иодепи поридна ЗО пин

Верификация процедуры Затраты времени ка вери<*ииации> одной процедуры порядна J 0 с

Состав модулейа

— программа управления;

— графический редактор|

— библиотека графических элементов)

— блон вериФМнации|

— база готовых моделей|

— блон печати.

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

, Заключение

г

1. Про«налмэнроеанкы современные методы проектирования нолгпей офисным систем и языки спецификации офисным процедур с позиций автоматизации проектирования с использованием логического подхода, показано, что наСболее перспективными для автоматизированной периФикации офисным процедур являются методы, базирующиеся на спецификации офисным процедур с использованием обобщенным логических коннекторов. í?. Разработан язык спецификации офисным процедур, сочетающий средства методологии гроектирова^ля CSIRXS и COSE-текнопогии, б&эирующейся не инструментальной системе COSE—Пнапитин, в результате чего обеспечена возможность автоматизированного проектирования спецификаций офисным процедур, интеграции офисным процедур в систему и графического' представления спецификаций.

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

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

3. Соаданы инструментальные средства поддержки языка спецификации и процессов верификации офисным процедур на базе системы CRSE—Аналитик в треде Window» и операционной среде MS-DOS для ПЭВМ типа IBM PC. 6.Разработанные инструментальные средства и методы автоматизированного проектирования офхсных процедур внедрены при автоматизированном проектировании передвижного комплекса для подготовки А обогащению алмазосодержащим глинистым песков месторождения

-го-

"Горно»" Мирненского ПОКа Акционерной нонплиии "iVih .ui РОССИИ—СЙХД", а также в учебном процессе прч иурсш.м! и диплоинон проектировании систем упраелч-нии в МГГ> и Северо—Кавказском горно—металлургическом института.

Основные положения диссертации апубпиииснлны ь следующих работай I

1. Матюнина O.E. Модели о.чсным процедур и н ./г г. .-¡i .i ик верификации //Всемирный конгресс ■ IIS— *'ИНФорнационные коммуникации, сети, системы и технологии". Доклады. Москва. S3—BB ноябри, 1992.

2. Матюнина O.E. Методы иен у сстое кно г а интелпеит.» при верификации офиснын процедур//Отчет н-ДФедры "Вычислительные мамины*' по Госбюджетной тем* НИР "Проблемы искусственного интеллект« а СЙПР r-opnoii промышленности".М.1 МГГУ, 1993.

3. Рякин О. М. , Матюнина О.Е. Спецификация офисным процедур с использованием языковым средств системы COSE-йналитии //Всемирный конгресс ITS-ЭЗ "Информационные коммуникации, сети, системы и технологи«". Москве, 25-26 ноября, 1993.

А. Рянин О. М. , Матюнина O.E. Проблемы обучение методологии системного анализа «//Международная научно-техническая конференция "Развитие и применение отнрыгым систем". Тезисы докладов. Казань, 12-IV сентября, 199-1.

Под- исано в печать II. 01е 95# Формат ЬОнЭО^1& Объем 1 п. л. Тираж ЮО экз. Заказ N

Типография Московского горного университета

М., Ленинский пр-т, 0