Введение к работе
Актуальность темы. При использовании современных методов автоматизированного проектирования распределенных информационных систем в ходе анализа и синтеза проектных процедур реализации межинтерфейсного взаимодействия один шаг в низкоуровневой спецификации может быть верифицирован расширенным выполняемым фрагментом на более высоком уровне. Вследствие этого автоматизация таких методов с использованием универсальных средств доказательства теорем является трудноразрешимой задачей.
Операторные отображения и функции детализации широко используются для доказательства того, что низкоуровневая спецификация проектируемой системы корректно реализует высокоуровневую. Непротиворечивость доказательства и полнота правил проверки отображения и детализации оказались чрезвычайно важными при выполнении автоматизированного семантического анализа проектных процедур.
Нередко применяемые методологии анализа проектных процедур, связанные с семантическими сетями, сетями Петри, автоматным моделированием, позволяют решать задачу проектного анализа корректности процедур только при масштабном взаимодействии с лицом, принимающим решение.
Методологии структурного и объектно-ориентированного программирования, активно применяющиеся в процедурах проектного синтеза для автоматизации проектирования межмодульных интерфейсов информационных систем, не позволяют в полной мере провести проектную верификацию результатов проектирования. Сравнительно давно используется и метод "автоматного" программирования, особенностью которого является то, что в основу проектирования программы закладывается алгоритм - конечный автомат в виде диаграммы состояний, или таблицы последовательных переходов и выходов. Однако и в случае применения «автоматного» программирования в процессе автоматизированного проектирования верификация результатов также затруднена.
Таким образом, актуальна проблема теоретического обоснования, разработки и внедрения средств анализа и синтеза корректирующих проектных решений по автоматизации процедур верификации межмодульного взаимодействия при проектировании информационных систем на основе операторного моделирования. Разработка такого программного обеспечения анализа и синтеза позволит снизить затраты и ускорить процесс проектирования распределенных информационных систем.
Работа выполнена в соответствии с научным направлением ГОУВПО «Липецкий государственный технический университет» "Информационные системы и базы данных".
Цель работы. Целью работы является теоретическое обоснование, разработка и внедрение автоматизированных процедур анализа и синтеза
средств верификации межмодульного взаимодействия при автоматизированном проектировании информационных систем на основе операторного моделирования.
Задачи исследования. Для достижения поставленной цели необходимо решить следующие задачи:
исследовать с позиций системного анализа место и роль процедур проектной верификации в системах автоматизации проектирования инструментов межинтерфейсного взаимодействия распределенных информационных систем;
разработать теоретические основы построения процедур анализа проектируемых межмодульных интерфейсов на основе нормированных операторных отображений как инвариантов моделей интерфейсных компонент;
предложить элементы математического и лингвистического обеспечения корректирующих проектных решений подсистемы автоматизации верификации межмодульных интерфейсов;
создать алгоритмы верификации проектируемых межмодульных интерфейсов с применением операторного моделирования для построения нормированных прямых и обратных отображений межуровневых спецификаций межмодульных переходов;
разработать программные средства анализа и синтеза проектных решений по верификации межмодульного взаимодействия при автоматизированном проектировании распределенных информационных систем с применением операторного моделирования.
Методы исследования. В работе использованы методы системного анализа, автоматизированного проектирования, теории множеств, теории графов, дискретной математики, математической статистики, конечных автоматов, объектно-ориентированного программирования.
Научная новизна работы. К результатам работы, отличающимся научной новизной, относятся:
- метод формального анализа проектных решений по реализации ме
ханизмов межмодульного взаимодействия, отличающийся использованием
нормированных операторных отображений в качестве инвариантов интер
фейсных компонент;
-способ анализа конкретного операторного выражения на принадлежность классу нормированных прямых отображений, основанный на ряде теорем об инвариантности и корректности;
-алгоритм синтеза проектных решений по реализации межмодульного взаимодействия, отличающийся совместным использованием нормированных прямых и обратных отображений для спецификаций верхнего уровня, содержащих конечный неявный недетерминизм;
- алгоритм верификации межмодульного взаимодействия как основы
принятия корректирующих проектных решений, отличающийся примене-
ниєм операторного моделирования для построения межмодульных переходов;
-элементы математического и лингвистического обеспечения подсистемы анализа и синтеза проектных решений по верификации результатов проектирования межмодульных интерфейсов, отличающиеся использованием нормированных прямых и обратных отображений для спецификаций верхнего уровня, содержащих конечный неявный недетерминизм.
Практическая значимость работы.
Практическая значимость работы состоит в создании на основе разработанных методов и алгоритмов имплементируемых процедур анализа и синтеза корректирующих проектных процедур верификации межмодульного взаимодействия, позволяющих автоматизировано верифицировать функционирование сложных информационных систем.
Использование данного программного обеспечения позволяет сократить время, требуемое для автоматизированного проектирования и верификации информационных систем.
Результаты внедрения. Результаты исследований апробированы при проектировании специализированных информационных систем 'ТУК Правобережная" (г. Липецк), издательства «Научная книга» (г. Воронеж), а также в учебном процессе ГОУВПО «Липецкий государственный технический университет» на кафедре «Прикладная математика».
Апробация работы. Основные положения диссертационной работы докладывались и обсуждались на 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 рисунков.
