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

мйЯР

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

КОРЧАГИН Александр Сергеевич

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

Специальность: 05.13.12 - Системы автоматизации

проектирования

АВТОРЕФЕРАТ

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

1 О ДЕК 2009

Воронеж - 2009

Работа выполнена в ГОУВПО «Липецкий государственный технический университет»

Научный руководитель доктор технических наук, профессор

Погодаев Анатолий Кирьянович

Официальные оппоненты: доктор технических наук, профессор

Макаров Олег Юрьевич;

кандидат технических наук, доцент Мачтаков Сергей Геннадьевич

Ведущая организация ГОУВПО «Сибирский государствен-

ный аэрокосмический университет им. академика М.Ф. Решетнева»

Защита состоится 18 декабря 2009 года в 1430 часов в конференц-зале на заседании диссертационного совета Д 212.037.03 ГОУВПО «Воронежский государственный технический университет» по адресу: 394026, г. Воронеж, Московский просп., 14.

С диссертацией можно ознакомиться в научно-технической библиотеке ГОУВПО «Воронежский государственный технический университет».

Автореферат разослан «17» ноября 2009 г.

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

Родионов О.В.

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

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

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

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

Методологии структурного и объектно-ориентированного программирования, активно применяющиеся в процедурах проектного синтеза для автоматизации проектирования межмодульных интерфейсов информационных систем, не позволяют в полной мере провести проектную верификацию результатов проектирования. Сравнительно давно используется и метод "автоматного" программирования, особенностью которого является то, что в основу проектирования программы закладывается алгоритм - конечный автомат в виде диаграммы состояний, или таблицы последовательных переходов и выходов. Однако и в случае применения «автоматного» программирования в процессе автоматизированного проектирования верификация результатов также затруднена.

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

Работа выполнена в соответствии с научным направлением ГОУВПО «Липецкий государственный технический университет» "Информационные системы и базы данных".

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

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

Задачи исследования. Для достижения поставленной цели необходимо решить следующие задачи:

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

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

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

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

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

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

Научная новизна работы. К результатам работы, отличающимся научной новизной, относятся:

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

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

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

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

нием операторного моделирования для построения межмодульных переходов;

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

Практическая значимость работы.

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

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

Результаты внедрения. Результаты исследований апробированы при проектировании специализированных информационных систем 'ТУК Правобережная" (г. Липецк), издательства «Научная книга» (г. Воронеж), а также в учебном процессе ГОУВПО «Липецкий государственный технический университет» на кафедре «Прикладная математика».

Апробация работы. Основные положения диссертационной работы докладывались и обсуждались на XII Международной открытой научной конференции «Современные проблемы информатизации в моделировании и анализе сложных систем» (Воронеж, 2007); XIII и XIV Международной открытой научной конференции «Современные проблемы информатизации в моделировании и социальных технологиях» (Воронеж, 2008, Орел, 2009); XIII Международной открытой научной конференции «Современные проблемы информатизации в проектировании и информационных системах» (Воронеж, 2008); Всероссийской конференции «Новые технологии в научных исследованиях, проектировании, управлении, производстве» (Воронеж, 2008); XIV Международной открытой научной конференции «Современные проблемы информатизации в анализе и синтезе программных и телекоммуникационных систем» (Орел, 2009); научно-тематическом семинаре ГОУВПО «Липецкий государственный технический университет» "Информационные системы и базы данных" (Липецк, 2007-2009).

Публикации. По теме диссертации опубликовано 12 научных работ, в том числе 5 - в изданиях, рекомендованных ВАК РФ. В работах, опубликованных в соавторстве и приведенных в конце автореферата, лично соискателю принадлежат: [2, 8, 9] - метод формального анализа проектных решений по реализации механизмов межмодульного взаимодействия; [7, 10] - способ анализа конкретного операторного выражения на принадлежность классу нормированных прямых отображений; [1, 5, 6] - алгоритм

синтеза проектных решений по реализации межмодульного взаимодействия; [4,9,10] - алгоритм верификации межмодульного взаимодействия как основы принятия корректирующих проектных решений; [3, 4, 11, 12] -элементы математического и лингвистического обеспечения подсистемы анализа и синтеза проектных решений по верификации результатов проектирования межмодульных интерфейсов.

Структура и объем работы. Диссертация состоит из введения, четырех глав, заключения, списка литературы из 105 наименований. Основная часть работы изложена на 149 страницах, содержит 3 таблицы и 37 рисунков.

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

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

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

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

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

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

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

Рис. 1. Место компонент верификации межмодульных интерфейсов в составе САПР

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

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

Автомат (или система помеченных переходов) А состоит из:

- (возможно, бесконечного) множества состояний

- непустого множества начальных состояний Иап(А) схШ1ех(А);

- множества операций ас/з(А), с внутренней операцией г;

- множества переходов $1ерз(А) cr.itaie.sf/lj х ас&(А) х Ш/е5(Д).

Обозначим 5——как сокращение для (з,а,г)е в1ер$(А). Обозна-

чим ext(A), внешние операции, как acts(A) - т. Выполняемый фрагмент А есть конечная или бесконечная меняющаяся последовательность s0aisia2s2... состояний и операций А, начинающаяся с состояния и, если она конечна, оканчивающаяся также состоянием, так что для всех

i > 0,5(1—3—>st. Исполнение А есть выполняемый фрагмент, начинающийся с начального состояния. Обозначим через execs (А) и execs(A) множества конечных и всех исполнений А, соответственно. Некоторое состояние s автомата А является достижимым, если s является последним состоянием в некотором конечном выполнении А- а. Этот случай обозначим как reachable(A,s). Будем использовать также reachable(A) для обозначения множества достижимых состояний А.

След исполняемого фрагмента а, обозначаемый trace(a), - подпоследовательность отличных от г операций, выполняемых в а. Конечная или бесконечная последовательность внешних операций /? является следом А, если у А есть исполнение а с /?= trace(a). Множества конечных и всех следов А обозначаются, соответственно, traces (А) и traces(A). А < --¡В означает, что traces'(A)œ traces'(В), и А < ТВ означает, что traces(A)ç traces(B).

Предположим, что А - автомат, s и / - состояния А, а Р - конечная последовательность над ext(A). Говорят, что (s, f},t) есть переход в А и это

Р Р

обозначается как J =>л t или просто s=>t, когда ясно, что речь идёт об А, если у А существует конечный исполняемый фрагмент а, начинающийся в 5, заканчивающийся в / и имеющий след р.

Важную роль играют три типа автоматов с ограничениями:

1. А является детерминированным, если \start(Aj\ = 1 и для любого состояния s и любой конечной последовательности р над ext(A) существует

только одно состояние t такое, что s=>t. Детерминированный автомат характеризуется однозначно тем свойством, что \start(A)\ = 1, каждый г- шаг имеет вид (s, t,s) для некоторого s, и для каждого состояния s и операции а существует не более одного состояния t такого, что s——>л t.

2. У А есть конечный неявный недетерминизм (fin), если start(A) конечно, и для любого состояния s и любой конечной последовательности р над ext(A) существует лишь конечное множество состояний t таких, что

Р

S=>at .

3. А есть лес, если для каждого состояния 5 автомата А существует точно одно выполнение, приводящее к s. Лес однозначно характеризуется тем свойством, что все состояния А достижимы, начальные состояния не имеют входящих шагов, и каждое состояние, не являющееся начальным, имеет ровно один входящий шаг.

Отношение after(A) состоит из пар (p,s), для которых существует ко-

нечное выполнение А со следом /? и последним состоянием s:

л

after(A)={(fl,s)\3a е execs' (А) : tracera) = р и last(a) = s}.

Здесь last обозначает функцию, возвращающую последний элемент конечной непустой последовательности. Определим past(A) как обратную

л

к after(A), past(A) = after (А)~ , это определяет соотношение между состоянием s автомата А и следами конечных выполнений А, приводящих к s.

Лемма 1.

1. Если автомат А детерминированный, то after(A) есть функция, действующая из traces'(А) в states(A).

2. Если у А есть fin, то after(A) является конечным отображением, т.е. каждый след в области определения after(A) связан с конечным числом состояний.

3. Если А - лес, то past(A) - функция из states(A) в traces'(А).

Пусть А и В - автоматы. Пошаговая детализация из А в В- частично вычислимая функция г из states(A) в states(B), удовлетворяющая следующим двум условиям:

1. Если s estart(A), то sedomain(r) и r(s) е start(B).

2. Если 5 ——>.t I л s е domain(r), то tedomain(r) и

(a) r(s)=r(t) л a= t

(b) r(s)-=-*er(/).

Пишем A <„ В, если существует пошаговая детализация из А в В.

Следующее утверждение устанавливает основное свойство корректности пошаговой детализации.

Теорема 1. Отношение <r есть отношение порядка (т.е. транзи-тивно и рефлексивно).

Рис. 2 иллюстрирует понятие пошаговой детализации, г-шагам в А не соответствует ни один шаг в В. Также и с-шагу в А не соответствует ни один шаг в В: и исходное, и конечное состояния этого шага находятся вне области определения пошаговой детализации. Это можно допустить, поскольку оба состояния недостижимы. Не существует пошаговой детализации из В в А, но существует вероятностное отображение из В в А.

Если существует пошаговая детализация из А в В, то можно построить для каждого выполняемого фрагмента А соответствующий выполняемый фрагмент В с той же трассой. Понятие «соответствующий» формализовано ниже.

Предположим, что А и В - автоматы, R çr states(A) * states(B), и а = SoajS/a2S2 и а' = uobiu/biut - выполняемые фрагменты А и В, соответственно. Пусть index (а) и index (а') обозначают множества индексов а и а'. Тогда а и а' соответствуют посредством R и являются R-связанными, что обозначается как (а, а') е R, если существует отношение индексов над R, т.е. отношение 1er index(a) х indexfa') такое,что

(1) если два индекса связаны отношением /, то соответствующие состояния связаны отношением Л;

(2) / монотонно;

(3) каждый индекс из а связан с индексом из а' и наоборот;

(4) стороны «квадратов» всегда имеют одинаковую метку, а стороны «треугольников» помечены буквой т.

Рис. 2. Пошаговая детализация

Формально требуем для /, Г е index (а) и j,j' е index (а'),

1. (i,j) el =>(sh uj eR

2. (i J) e I л (i\f) e I Ai< V =>j <f

3. / и Г' являются полными

(/,» е / Л(/ +1,7 +1) е / => = bJtX

('.У) 6 / л (/ + е / => а,,, = г

0,j) е / л (i,j +1) е / => ¿)tl = г

Записываем f^.Sj е /? , если для каждого выполнения а автомата А существует выполнение а' автомата В такое, что (а, а') е R, и [А,В] е R, если для каждого конечного выполнения а из А существует конечное выполнение а' из В, причём (а, а') е R. Рис. 3 иллюстрирует соответствие между двумя выполнениями автоматов А и В, изображённых на рис. 2.

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

Теорема 2. (Семантическая непротиворечивость пошаговых уточнений). Если г - пошаговая детализация из А в В, то (А,В) е г.

Далее в работе введено понятие нормированного прямого отображения. Нормированное прямое отображение из А в В состоит из отношения fc states(A)xstates(B) и функции п: steps(A) *states(B)—>S для некоторого вполне определенного множества S такого, что:

1. Если s е start (A), mof[s] П start (В)

2. Если s—^.((лие/[s],TO

(a) ие/Мли = г,или

(b) 3v6 Л«1 :«-=-♦« vfHJIII

3ve/Is]:и—r—yevAn(s—*—n,v)<n(s——*t,u) Здесь ffsj означает множество {u| (s,u)ef). * s3 b 34

и 0 ° 112 * и2 Т и2

Рис. 3. Соответствие выполнения

Пишем А <р В, если существует нормированное прямое отображение из А № В.

Из определения понятно, что если *—^ <' и и) е/, то или (а) переход в А является редуцирующим шагом, которому не должно ничто соответствовать, или (Ь) существует соответствующий шаг в В, или (с) в В может быть выполнен редуцирующий шаг, который уменьшает норму. Поскольку норма уменьшается при каждом применении утверждения (с), это утверждение можно применять только конечное число раз. В общем случае функция нормы может зависеть и от переходов в А, и от состояний В. Однако, если В является конвергентным, т.е. отсутствуют бесконечные т-пути, можно упростить тип функции нормы до п: $1а1е$(В)—>5.

Показано, что нормированные прямые модели действительно пошаговые детализации: А <„ В Л <Р В.

Семантическая непротиворечивость нормированных прямых моделей тривиально вытекает из следующей леммы.

Лемма 2. Пусть (/,п) - нормированное прямое отображение из А в В, в А есть выполняемый фрагмент а с начальным состоянием 5. и и - состояние В, причём ие/[$]. Тогда в В есть выполняемый фрагмент а', начинающийся в и, такой, что (а, а') е/.

Теорема 3. (Непротиворечивость нормированных прямых отображений). Если/- нормированная прямая модель из А в В, то (А, В) е/

Формально определим, что нормированное обратное отображение из

А в В представляет пару:

{Ъ Sstates(A) * states(B); функция п : (steps(A) U start (А)) * states (В) или некоторое вполне определенное множество, удовлетворяющее следующему условию:

1. Если s е start (А) Л и eb[s], тогда

(a) и б start (В), или

(b) 3 V 6 ¿>[s]: V ——»в ч Л n(s, v) < n(s, и).

2. Если t —i->As Л u е b[s],тогда

(a) u е b[t] Л а = т, или

(b) 3 v g b[t]: v —В и, или

(c) 3ve b[s]: v —i-> В иЛ n(t —v) <n(t —=->s, u).

Запишем А <в В , если имеется нормированное обратное отображение из А в В и A Sb В, если это нормированное обратное отображение из А в В является конечно-образным.

Теорема 4.

1. Если все состояния А достижимы и A <R В, то А ¿т В.

2. Если А ¿,вВ, тогда А ¿в В.

Теорема 5. (Корректность нормированных обратных отображений).

1. Если b - нормированные обратные отображения из А в В, то [А,В]еЬ.

2. Если b является конечно-образным, то (А,В)еЬ.

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

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

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

Декомпозиция задач ! межмодульного взимоденствия

Выбор очередной I1MI3

/лапергпепие^ синтеза ^J

Рис. 4. Структурная схема алгоритма реализации корректирующих проектных решений: ПМВ - процедура межмодульного взаимодействия

Элементы математического и лингвистического обеспечения созданы для имплементации в библиотеку системы ToolBus управления архитектурой информационных систем с использованием языка PSF (Process Specification Formalism). Описание элемента данных (тип):

data module TooUypes begin exports begin

sorts

Tterm end end ToolTypes

Типы введены для объектов данных и идентификаторов, которые будут использоваться как внутри, так и вне ToolBus: data module ToolBusTypes begin exports begin

sorts

TBterm, TBid end end ToolBusTypes

Объект Tool Functions обеспечивает преобразование между терминами данных, используемыми внутри и вне ToolBus. data module ToolFunctions begin exports begin

functions

tbterm : Tterm -> TBterm

tterm : TBterm -> Tterm end imports

ToolTypes, ToolBusTypes

variables

t: -> Tterm equations

['] tterm (tbterm (t)) =t end ToolFunctions

На рис. 5 показаны два способа интерфейсного взаимодействия разрабатываемых проектных процедур с ToolBus.

Рис. 5. Механизмы интерфейсного взаимодействия разрабатываемых проектных процедур с ТооШиБ

Определим объект, обеспечивающий это взаимодействие, process module ToolAdapterPrimitives begin exports begin

atoms

tooladapter-rec: Tterm tooladapter-snd: Tterm

end

imports

ToolTypes end ToolAdapterPrimitives

Наконец, определим средство для описания инструментов: data module Data begin

exports begin

functions

message : -> Tterm ack: -> Tterm quit: -> Tterm

end

imports

ToolTypes

end Data

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

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

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

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

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

Подсистема декомпозиции задач межмодульного взаимодействия

X

ЛПР

Генератор кода формализованных 11МФ

Подсистема анализа результатов моделирования

Блок имплементации

Модуль | верификации ;

Блок формирования условий имитационного эксперимента

■I ToolBus f

СУБД проектных процедур

Рис. 6. Укрупненная структура ПО анализа и синтеза проектных ре-

шении

Рис. 7. Типичный сценарий верификации спецификации

Для реализации программного комплекса использован объектно-ориентированный язык С++ и среда визуального проектирования Borland С++ Builder. Программный комплекс рассчитан на работу под управлением операционной системы семейства Windows. Его функционирование возможно при наличии установленного драйвера ODBC и СУБД Microsoft SQL

Server2000. Комплекс внедрён в ООО 'ТУК Правобережная" (г. Липецк).

is ToolBus У1СЫ8Г <a»aipl«.tb> д-1 Options

■ process PT1 is let

T1: toon adapter, D term, R :term

in

executeftooil adapter, T1?). (

Tec-event(Tl, D?) (

if equal(D, quit) then shutdown("")

(i

+ if not(equal(D, quit)) then snd-msg(ti, t2, D). rec-msg(l2, tl, R?).

Нале:

Stop

pti ртг

jO

п

tool2

I Л

jp9 toolladapter

(received 'nessage* fron tool isendine to ToolBus ¡received ack Ггоп ToolBus sending to tool

GD tooll

send nwsacB quit !

Step

a toott

¡received 'nessaee' ^sending *ack*

tooll adapter

Рис. 8. Комбинированная экранная форма, иллюстрирующая процесс моделирования и верификации

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

Структура системы управления Web-контентом "Научный журнал" представлена на рис. 9. Ядро системы состоит из клиентской и административной части и реализовано с использованием объектно-ориентированного языка С++ и среды визуального проектирования Borland С++ Builder, а также PHP для серверных компонент. Система внедрена в ООО Издательство «Научная книга» (г. Воронеж).

Теоретические, лингвистические и алгоритмические компоненты использованы при верификации сложной программной системы иденти-

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

Рис. 9. Общая структура системы управления \УеЬ-контентом

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

Модульная структура ПО включает в себя 4 раздела, отвечающих за ввод исходных данных, расчёт выходных параметров, вывод и хранение полученных результатов и обработку ошибок. Программная система обеспечивает процессы: приема вводимых параметров системы; определения вероятностно-временных характеристик в заданном режиме работы; визуального отображения введенных параметров и рассчитанных характеристик системы; сохранения результатов расчета.

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

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

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

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

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

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

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

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

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

Основные результаты диссертации опубликованы в следующих работах:

Публикации в изданиях, рекомендованных ВАК РФ

1. Говорский А.Э. Параметрический синтез гетерогенной интегральной корпоративной информационно-управляющей системы / А.Э. Говорский, О.Я. Кравец, A.C. Корчагин // Системы управления и информационные технологии. 2008. 3.1(33).-С. 128-134.

2. Корчагин A.C. О связи нормированных прямых и обратных отображений / A.C. Корчагин, А.К. Погодаев // Системы управления и информационные технологии. 2008. 3.2(33). - С. 283-287.

3. Говорский А.Э. Проектирование программной системы идентификации характеристик неоднородных систем с интеграцией служб / А.Э. Говорский, Н.Ф. Жданов, A.C. Корчагин // Системы управления и информационные технологии. 2009. 2.1(36) - С. 204-208.

4. Корчагин A.C. Автоматизация проектирования и верификации компонент программной системы электронного документооборота на основе автоматного подхода / A.C. Корчагин, С.Г. Клименко // Системы управления и информационные технологии. 2009. 2.1(36).-С. 136-140.

5. Погодаев A.K. Автоматизация проектирования подсистемы верификации межмодульных интерфейсов информационных систем / А.К. Погодаев, A.C. Корчагин, О.Я. Кравец // Системы управления и информационные технологии. 2009. №3.1<37). - С. 203-208.

Статьи и материалы конференций

6. Корчагин A.C. Доказательство корректности программ на основе применения нормированных моделей / А.К. Погодаев, A.C. Корчагин // Прикладные задачи моделирования и оптимизации: межвуз. сб. науч. тр. Воронеж: ВГТУ, 2006. С. 186-195.

7. Корчагин A.C. К методологии операторного моделирования при исследовании корректности программ / А.К. Погодаев, A.C. Корчагин // Информационные технологии моделирования и управления. 2007. № 3(37). -С. 363-370.

8. Кравец О.Я. О непротиворечивости нормированных прямых моделей / О.Я. Кравец, A.C. Корчагин // Современные проблемы информатизации в проектировании и информационных системах: сб. тр. Воронеж: Научная книга, 2008. Вып. 13. - С. 494-497.

9. Кравец О.Я. О свойствах обратных отображений с ветвлениями / О.Я. Кравец, А.К. Погодаев, A.C. Корчагин // Современные проблемы информатизации в моделировании и социальных технологиях: сб. тр. Воронеж: Научная книга, 2009. Вып. 14. - С. 236-239.

10. Кравец О.Я. О взаимосвязи между отношениями порядка, нормированными обратными отображениями и пошаговой детализацией ветвлениями / О.Я. Кравец, A.C. Корчагин, А.К. Погодаев // Современные проблемы информатизации в анализе и синтезе программных и телекоммуникационных систем: сб. тр. Воронеж: Научная книга, 2009. Вып. 14. С. 319322.

11. Корчагин A.C. Программная реализация комплекса для проведения вычислительного эксперимента по анализу плана ремонтных работ / A.C. Корчагин, А.К. Погодаев // Информационные технологии моделирования и управления. 2009. № 4(56). - С. 605-612.

12. Корчагин A.C. Особенности разработки и верификации программного обеспечения системы управления научным журналом / A.C. Корчагин, О.С. Свиридова, О.Я. Кравец // Информационные технологии моделирования и управления. 2009. № 4(56). - С. 492-502.

Подписано в печать 16.11.2009. {

Формат 60x84/16. Бумага для множительных аппаратов. Усл. печ. л. 1,0. Тираж 90 экз. Заказ № т

ГОУВПО «Воронежский государственный технический университет» 394026 Воронеж, Московский просп., 14

Введение

Содержание

1. Анализ процессов автоматизации проектирования средств межинтерфейсиого взаимодействия в распределенных информационных системах.

1.1. Анализ подходов к автоматизации проектирования информационных систем с помощью операторного моделирования.

1.2. Технология проектирования с явным выделением состояний

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

1.4. Постановка задач исследования.

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

2.1. Пошаговая детализация операторных отображений низкоуровневых спецификаций.

2.2. Свойства нормированного прямого отображения, использующего пошаговую детализацию.

2.3. Обратные операторные модели.

2.4. Выводы.

3. Элементы математического и лингвистического обеспечения корректирующих проектных решений.

3.1. Проектный этап реализации процедур анализа и синтеза средств верификации.

3.2. Методология и алгоритмизация описания и построения корректирующих проектных решений.

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

3.4. Лингвистическое обеспечение межинтсрфейсного взаимодействия.

3.5. Выводы.

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

4.1. Особенности реализации алгоритмов анализа и синтеза.

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

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

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

4.5. Выводы.

Актуальность темы

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

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

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

Методологии структурного и объектно-ориентированного программирования, активно применяющиеся в процедурах проектного синтеза для автоматизации проектирования межмодульных интерфейсов информационных систем, не позволяют в полной мере провести проектную верификацию результатов проектирования. Сравнительно давно используется и метод "автоматного" программирования, особенностью которого является то, что в основу проектирования программы закладывается алгоритм - конечный автомат в виде диаграммы состояний, или таблицы последовательных переходов и выходов. Однако и в случае применения «автоматного» программирования в процессе автоматизированного проектирования верификация результатов также затруднена.

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

Работа выполнена в соответствии с научным направлением ЛГТУ "Информационные системы и базы данных".

Цель работы

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

Задачи исследования

Для достижения поставленной цели необходимо решить следующие задачи:

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

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

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

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

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

Методы исследования

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

Научная новизна работы

К результатам работы, отличающимся научной новизной, относятся:

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

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

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

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

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

Практическая значимость работы

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

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

Результаты внедрения

Результаты исследований апробированы при проектировании специализированных информационных систем "ГУК Правобережная" (г.Липецк), издательства «Научная книга» (г.Воронеж), а также в учебном процессе Липецкого государственного технического университета на кафедре «Прикладная математика».

Апробация работы

Основные положения диссертации докладывались и обсуждались на: XII-й Международной открытой научной конференции «Современные проблемы информатизации в моделировании и анализе сложных систем» (Воронеж, 2007), XIII-й и XIV-й Международной открытой научной конференции «Современные проблемы информатизации в моделировании и социальных технологиях» (Воронеж, 2008, Орел, 2009), XIII-й Международной открытой научной конференции «Современные проблемы информатизации в проектировании и информационных системах» (Воронеж, 2008), Всероссийской конференции «Новые технологии в научных исследованиях, проектировании, управлении, производстве» (Воронеж, 2008); XIV-й Международной открытой научной конференции «Современные проблемы информатизации в анализе и синтезе программных и телекоммуникационных систем» (Орел, 2009), научно-тематическом семинаре ЛГТУ "Информационные системы и базы данных" (Липецк, 2007-2009).

Публикации

По материалам диссертации опубликовано 12 научных работ, в том числе 5 - в изданиях, рекомендованных ВАК РФ. В работах, опубликованных в соавторстве и приведенных в конце автореферата, лично соискателю принадлежат: в [2, 8, 9] - метод формального анализа проектных решений по реализации механизмов межмодульного взаимодействия; в [7, 10] -способ анализа конкретного операторного выражения на принадлежность классу нормированных прямых отображений; в [1, 5, 6] - алгоритм синтеза проектных решений по реализации межмодульного взаимодействия; в [4, 9, 10] - алгоритм верификации межмодульного взаимодействия как основы принятия корректирующих проектных решений; в [3, 4, 11, 12] - элементы математического и лингвистического обеспечения подсистемы анализа и синтеза проектных решений по верификации результатов проектирования межмодульных интерфейсов.

Структура и объем работы

Диссертация состоит из введения, четырех глав, заключения, списка литературы из 105 наименований. Основная часть работы изложена на 149 страницах, содержит 3 таблицы и 37 рисунков.

4.5. Выводы

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

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

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

Заключение

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

Для достижения поставленной цели были решены следующие задачи:

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

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

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

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

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

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

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

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

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

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

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

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

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

Результаты исследований апробированы при проектировании специализированных информационных систем "ГУК Правобережная" (г.Липецк), издательства «Научная книга» (г.Воропеж), а также в учебном процессе Липецкого государственного технического университета на кафедре «Прикладная математика».

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

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

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

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

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

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

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

1. Авен О.И., Гурнн Н.Н., Коган Я.А. Оценка качества и оптимизация вычислительных систем. — М.: Наука, 1982.

2. Анализ и синтез сложных технических систем. В 2-х ч., 4.1. М.: Воениздат, 1995.-401 с.

3. Ахо А., Ульман Дж. Теория синтаксического анализа, перевода и компиляции. В 2-х томах. М.: Мир. 1978.

4. Байцер Б. Архитектура вычислительных комплексов. Том 1. М.: Мир. 1974.

5. Баранов С.И. Синтез микропрограммных автоматов. Л.: Энергия. -1979.

6. Бек К. Экстремальное программирование. Библиотека программиста. СПб.: Питер, 2002. - 224 с.

7. Боггс У., Боггс М. UML и Rational Rose. М.: Лори, 2001. - 608 с.

8. Брукс Ф. Мифический человеко-месяц, или как создаются программные системы,- СПб.: Символ-Плюс, 2005.-304 с.

9. Буч Г. Объектно-ориентированный анализ и проектирование с примерами приложений на С++. М.: "Изд-во Бином", СПб: "Невский диалект". 1998.

10. Буч Г., Рамбо Д., Джскобсон А. Язык UML. Руководство пользователя. М.: ДМК.-2000.

11. П.Говорский А.Э. Распределенные информационные системы контроля и управления. СПб: Энергоатомиздат, Санкт-Петербургское отделение, 2004. - 378 с.

12. Говорский А.Э., Жданов Н.Ф., Корчагин А.С. Математическая модель гетерогенной интегральной корпоративной информационно-управляющей системы в дискретном времени// Системы управления и информационные технологии. №1.1(35), 2009. С. 139-144.

13. Говорский А.Э., Жданов Н.Ф., Корчагин А.С. Проектированиепрограммной системы идентификации характеристик неоднородных систем с интеграцией служб// Системы управления и информационные технологии, 2009, 2.1(36) С. 204-208.

14. Говорский А.Э., Корчагин А.С., Кравец О.Я. Параметрический синтез гетерогенной интегральной корпоративной информационно-управляющей системы// Системы управления и информационные технологии. №3.1(33), 2008. С. 128-134.

15. Говорский А.Э., Кравец О.Я. Математическое моделирование неоднородного трафика гетерогенной интегральной корпоративной информационно-управляющей системы// Системы управления и информационные технологии. №2.2(32), 2008. С. 228-234.

16. Говорский А.Э., Кравец О.Я., Повалясв А.Д. Подходы к моделированию неоднородных интегральных информационно-управляющих систем// Системы управления и информационные технологии, 2007, №3.1(29). -С. 131-138.

17. Говорский А.Э., Кравец О.Я., Суворов Д.В. Проблемы и особенности моделирования и рационального проектирования интегральных систем обслуживания неоднородного трафика// Системы управления и информационные технологии, 2007, №2.1(28). С. 122-129.

18. Гуров В., Нарвский А., Шалыто А. Исполняемый UML из России //PC Week/RE. 2005. - № 26. - С. 18-19.

19. Джамп Д. AutoCAD. Программирование. М.: Радио и связь.1992.

20. Константин JI. Человеческий фактор в программировании. СПб.: Символ-Плюс, 2004. - 384 с.

21. Корбут А.А., Финкелыптейн Ю.Ю. Приближенные методы дискретного программирования. // Изв. АН СССР: Техн. Кибернетика, 1963, №1. С. 165-176.

22. Корчагин А.С., Кравец О.Я. О состоянии проблемы проверки корректности систем и протоколов// Современные проблемы информатизации в моделировании и анализе сложных систем: Сб. тр. Вып. 13. Воронеж: Научная книга, 2007. - С. 198-207.

23. Корчагин А.С., Кравец О.Я. Операторное моделирование с использованием последовательной детализации при доказательстве корректности программ// Информационные технологии моделирования и управления, № 6(40), 2007. С. 714-719.

24. Корчагин А.С., Кравец О.Я., Погодаев А.К. О некоторых свойствах технологии пошаговой детализации при доказательстве корректности программ// Системы управления и информационные технологии, 2007, №3.1(29). С. 166-169. 2.2.4.

25. Корчагин А.С., Свиридова О.С., Кравец О.Я. Особенности разработки и верификации программного обеспечения системы управления научным журналом// Информационные технологии моделирования, и управления, № 4(56), 2009. С. 492-502.

26. Корчагин А.С., Погодаев А.К. Доказательство корректности программ на основе применения нормированных моделей// Прикладные задачи моделирования и оптимизации: Межвузовский сборник научных трудов. Воронеж: ВГТУ, 2006. С. 186-195.

27. Корчагин А.С., Погодаев А.К. Доказательство корректности программ на основе применения нормированных моделей// Прикладные задачи моделирования и оптимизации: Межвузовский сборник научных трудов. Воронеж: ВГТУ, 2006. С. 186-195.

28. Корчагин А.С., Погодаев А.К. К методологии операторного моделирования при исследовании корректности программ// Информационные технологии моделирования и управления, №3(37), 2007. С. 363-370.

29. Корчагин А.С., Погодаев А.К. О связи нормированных прямых и обратных отображений// Системы управления и информационные технологии, 2008, 3.2(33). С. 283-287.

30. Корчагин А.С., Погодаев А.К. Основы применения нормированных моделей для доказательства корректности программ// Информационные технологии моделирования и управления, № 6(31), 2006. С. 731-738.

31. Корчагин А.С., Погодаев А.К. Программная реализация комплекса для проведения вычислительного эксперимента по анализу плана ремонтных работ// Информационные технологии моделирования и управления, № 4(56), 2009. С. 605-612.

32. Корчагин А.С., Погодаев А.К. Технология пошаговой детализации при операторном моделировании для доказательства корректности программ// Территория науки, 2007, №4(5). Воронеж 2007. С. 501-507.

33. Кравец О.Я., Корчагин А.С. О связи прямого и нормированного прямого отображений// Информационные технологии моделирования и управления, 2008, №4(47). С. 392-398.

34. Кравец О.Я., Корчагин А.С. Об особенностях нормированных обратных отображений// Информационные технологии моделирования и управления, № 7(50), 2008. С. 796-803.

35. Кравец О.Я., Корчагин А.С. Операторное моделирование с использованием последовательной детализации при доказательстве корректности программ// Информационные технологии моделирования и управления, № 6(40), 2007. С. 714-719.

36. Кравец О.Я., Корчагин А.С., Погодаев А.К. О некоторых свойствах технологии пошаговой детализации при доказательстве корректности программ// Системы управления и информационные технологии, 2007, №3.1(29). С. 166-169.

37. Кравец О.Я., Корчагин А.С., Погодаев А.К. О свойствах нормированного прямого моделирования, использующего пошаговую детализацию// Информационные технологии моделирования и управления, № 9(43), 2007.-С. 1037-1041.

38. Кравец О.Я., Корчагин А.С., Погодаев А.К. О свойствах обратных отображений с ветвлениями. Современные проблемы информатизации в моделировании и социальных технологиях: Сборник трудов, выпуск 14. -Воронеж: «Научная книга», 2009. - С. 236-239.

39. Кравец О.Я., Свиридова О.С. Система управления Web-контентом "Научный журнал" // Информационные технологии моделирования и управления / Международный сборник научных трудов. Выпуск 15. Воронеж: Изд-во "Научная книга", 2003. - с. 61-65.

40. Кремер А.А, Корчагин А.С. Программный модуль «Модель многоуровневой реконфигурируемой системы». М.: ФАП ВНТИЦ, 2007. № ГР 50200701849 от 30.08.07.

41. Кузнецов Б.П. Стандартная реализация управляющих программ // Судостроительная промышленность. Сер. Системы автоматизированного проектирования 1986. с. 51 - 55.

42. Кузнецов О.П., Адельсон-Вельский Г.М. Дискретная математика для инженера. М.: Энергоатомиздат. 1988.

43. Маракушин М.В. Задача перспективного планирования ремонтно-восстановительных работ // Управление большими системами. 2006. -Вып. 14. С. 140-146.

44. Маракушин М.В., Томилов A.J1. Информационная система управления жилищным фондом // Системы управления и информационные технологии, 2007. № 1.1(27). С. 176-180.

45. Мартин Дж. Вычислительные сети и распределенная обработка данных: программное обеспечение, методы и архитектура. Вып. 1. - М.: Финансы и статистика, 1985. - 256 с.

46. Системное проектирование интегрированных программных комплексов. / Под ред. В.М. Пономарева. Д.: Машиностроение, 1996. - 336 с.

47. Срибнер JI.A. Программируемые устройства автоматики. К.: Технжа. 1982.

48. Татарчевский В.А. Применение SWITCH-технологии при разработке прикладного программного обеспечения для микроконтроллеров. Часть 1 // Компоненты и технологии. 2006. №11.

49. Татарчевский В.А. Применение SWITCH-технологии при разработке прикладного программного обеспечения для микроконтроллеров. Часть 2 // Компоненты и технологии. 2006. №12.

50. Татарчевский В.А. Применение SWITCH-технологии при разработке прикладного программного обеспечения для микроконтроллеров. Часть 3 // Компоненты и технологии. 2007. №1.

51. Фаулер М. UML. СПб.: Символ-Плюс, 2004. - 192 с.

52. Шалыто А.А. SWITCH-технология. Алгоритмизация и программирование задач логического управления. СПб.: Наука. 1998.

53. Шалыто А.А. Алгоритмизация и программирование задач логического управления. СПб.: СПбГУ ИТМО. - 1998. - 56 с.

54. Шалыто А.А. Еще раз об открытой проектной документации //PC Week/RE. 2005. - № 11, - С. 33-34.

55. Шалыто А.А. Использование граф-схем и графов переходов при программной реализации алгоритмов логического управления //Автоматика и телемеханика. 1996, - № 6. - С. 148 - 158; № 7. - С. 144— 169.

56. Шалыто А.А. Логическое управление. Методы аппаратной и программной реализации. СПб.: Наука, 2000. - 780 с.

57. Шалыто А.А. Новая инициатива в программировании. Движение за открытую проектную документацию //Мир компьютерной автоматизации. 2003. -№ 5. - С.67-71.

58. Шалыто А.А. Программная реализация управляющих автоматов// Судостроительная промышленность. Сер. «Автоматика и телемеханика». 1991. Вып. 13, с. 41-42.

59. Шеннон Р. Имитационное моделирование систем искусство и наука. - М.: Мир, 1988. - 634 с.

60. Шнейдерман Б. Психология программирования. М.: Радио и связь. 1984.

61. Abadi М., Lamport L. The existence of refinement mappings. Theoretical Computer Science, 82(2):253-284, 1991.

62. Bensalem Saddek, Ganesh Vijay, Lakhnech Yassine, et al. An overview of SAL. In C. Michael Iiolloway, editor, LFM 2000: Fifth NASA Langley Formal Methods Workshop, pages 187-196, Hampton, VA, jun 2000. NASA Langley Research Center.

63. Browne M.C., Clarke E.M., Grumberg O. Characterizing finite Kripke structures in Prepositional temporal logic. Theoretical Computer Science, 59(1,2):115-131, 1988.

64. Devillers M.C.A., Grioen W.O.D., Romijn J.M.T, Vaandrager F.W. Verification of a leader election protocol: Formal methods applied to IEEE 1394. Formal Methods in System Design, 16(3):307-320, June 2000.

65. Garland S.J., Lynch N.A., Vaziri M. IOA: A language for specifying, programming, and validating distributed systems, 1997. http://larch. lcs.mit.edu: 800 l/~garland/ioaLanguage. html.

66. Gawliclc R., Segala R., Sogaard-Andersen J.F., Lynch N.A. Liveness in timed and untimed systems. Technical ReportMIT/LCS/TR-587, Laboratory for Computer Science, MIT, Cambridge, MA, December 1993.

67. Ginzburg A. Algebraic Theory of Automata. Academic Press, New York-London, 1968.

68. Glabbeek R.J., Weijland W.P. Branching time and abstraction in bisimulation semantics. Journal of the ACM, 43(3):555-600, 1996.

69. Grioen W.O.D. Studies in Computer Aided Verification of Protocols. PhD thesis, University of Nijmegen, May 2000. Postscript and PVS sources available via http://www.cs.lam.nl/ita/former members/davidg/.

70. Groote J.F., Springintveld J.S. Focus points and convergent process operators — a Proof strategy for protocol verification. Report CS-R9566, Department of Software Technology, CWI, Amsterdam, November 1995. 1.3.10.

71. Guttag J.V., Horning J.J. Larch: Languages and Tools for Formal Specification. Springer-Verlag, 1993.

72. Harel D. Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming. 1987. Vol. 8, P. 231 -274.

73. Jonsson B. A model and Proof system for asynchronous networks. In Proceedings of the 4th Annual ACM Symposium on Principles of Distributed Computing, Minaki, Ontario, Canada, pages 49-58, 1985.

74. Jonsson B. Compositional specification and verification of distributed systems. ACM Transactions on Programming Languages and Systems, 16(2):259—303, March 1994.

75. Jonsson B. Compositional specification and verification of distributed systems. ACM Transactions on Programming Languages and Systems, 16(2):259—303, March 1994.

76. Jonsson B. Simulations between specifications of distributed systems. In J.C.M. Baeten and J.F. Groote, editors, Proceedings CONCUR 91, Amsterdam, volume 527 of Lecture Notes in Computer Science, pages 346-360. Springer-Verlag, 1991.

77. Klarlund N., Schneider F.B. Proving nondeterministically specified safety properties using progress measures. Information and Computation, 107(1): 151—170, November 1993.

78. Klarlund N., Schneider F.B. Verifying safety properties using infinite-state automata. Technical Report 89-1039, Department of Computer Sci-~ ence, Cornell University, Ithaca, New York, 1989.

79. Knuth D.E. Fundamental Algorithms, volume 1 of The Art of Computer Programming. Addison-Wesley, Reading, Massachusetts, 1997. Third edition.

80. Lamport L. What good is temporal logic? In R.E. Mason, editor, Information Processing 83, pages 657-668. North-Holland, 1983.

81. Lynch N.A. Distributed Algorithms. Morgan Kaufmann Publishers, Inc., San Fransisco, California, 1996.

82. Lynch N.A., Vaandrager F.W. Forward and backward simulations, I: Untimed systems. Information and Computation, 121(2):214-233, September 1995.

83. Manna Z., Browne A., Sipma H.B., Uribe Т.Е. Visual abstraction for temporal verification. In A.M. Haebercr, editor, Proceedings AMAST'98, volume 1548 of Lecture Notes in Computer Science, pages 28-41. Springer-Verlag, 1998.

84. Mueller О. A Verification Environment for I/O Automata Based on Formalized Meta-Theory. PhD thesis, Technical University of Munich, September 1998.

85. Nicola R. and Vaandrager F.W. Three logics for branching bisimulation. Journal of the ACM, 42(2):458-487, March 1995.

86. Nipkow Т., Slind K. I/O automata in Isabelle/PIOL. In P. Dybjer, B. Nordstrom, and J. Smith, editors, Types for Proof and Programs, volume 996 of Lecture Notes in Computer Science, pages 101-119. Springer-Verlag, 1995.

87. Owicki S., Grics D. An axiomatic Proof technique for parallel programs. Acta Informatica, 6(4):319-340, 1976.

88. Roever W.P., Engelhardt K. Data Refinement: Model-Oriented Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science 47. Cambridge University Press, 1998.

89. Sogaard-Andersen J.F., Lynch N.A., Lampson B.W. Correctness of communication protocols a case study. Technical Report MIT/LCS/TR-589, Laboratory for Computer Science, MIT, Cambridge, MA, November 1993.

90. Stark E.W. Proving entailment between conceptual state specifications. Theoretical Computer Science, 56:135-154, 1988.

91. Wolper Pierre. The meaning of formal: from weak to strong formal methods. Springer International Journal on Software Tools for Technology Transfer, l(l-2):6-8, 1997. 1.3.35.