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

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

При создании программных систем обычно выделяют следующие фазы:

1. Постановка задачи — сбор требований и создание прототипа программы.

2. Проектирование — разработка проектной документации, отражающей структурные и поведенческие особенности создаваемой системы.

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

4. Тестирование — отладка кода и проверка соответствия реализации поставленной задаче.

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

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

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

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

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

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

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

Цель диссертационной работы — разработка технологии проектирования и реализация объектно-ориентированных программ с явным выделением состояний.

Основные задачи исследования:

1. Создание метода проектирования объектно-ориентированных программ на основе автоматного подхода.

2. Разработка графического языка автоматного программирования.

3. Разработка методов верификации автоматных моделей программ.

4. Разработка инструментального средства для поддержки автоматного программирования.

5.Внедрение результатов работы в практику промышленной разработки программного обеспечения и в учебный процесс кафедры «Компьютерные технологии» СПбГУ ИТМО.

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

1. Метод проектирования объектно-ориентированных программ с явным выделением состояний.

2.Графический язык для описания автоматных программ на основе UML-нотации.

3.Методы верификации автоматных моделей программ: метод верификации на модели (Model Checking), а также метод верификации полноты и непротиворечивости систем переходов автоматов.

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

Перечисленные результаты получены в ходе выполнения в СПбГУ ИТМО научно-исследовательских и опытно-конструкторских работ по темам: «Разработка технологии создания программного обеспечения систем управления на основе автоматного подхода» (проводится по заказу Минобрнауки РФ с 2000 г. по настоящее время), «Разработка технологии автоматного программирования» (проводилась в 2002;2003 гг. по гранту Российского фонда фундаментальных исследований № 02−07−90 114), «Разработка технологии объектно-ориентированного программирования с явным выделением состояний» (проводилась в 2005;2006 гг. по гранту Российского фонда фундаментальных исследований № 05−07−90 011), «Технология автоматного программирования: применение и инструментальные средства» (государственный контракт, который выполнялся в 2005;2006 гг. в рамках Федеральной целевой научно-технической программы «Исследования и разработки по приоритетным направлениям развития науки и техники»). Последняя работа вошла в список 15 наиболее перспективных проектов, выполняемых по этой программе.

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

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

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

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

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

Упрощается верификация на основе метода Model Checking, так как в автоматных моделях состояния явно выделены, и поэтому пространство состояний по сравнению с программами, построенными традиционным образом, резко сокращается.

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

Внедрение результатов работы. Результаты, полученные в диссертации, используются на практике в компании eVelopers (Санкт-Петербург) при разработке интернет-приложений для электронной коммерции и мобильных устройств, а также в компании Intellij Labs (Санкт-Петербург) при разработке мета-программирования Meta Programming System.

Полученные результаты используются также в учебном процессе на кафедре «Компьютерные технологии» СПбГУ ИТМО при выполнении курсовых работ по курсу «Теория автоматов в программировании». При этом на сайте http://is.ifmo.ru в разделе UniMod-проекты опубликовано 28 проектов, выполненных с помощью предлагаемой технологии, которые содержат, в том числе, и проектную документацию.

Апробация диссертации. Основные положения диссертационной работы докладывались на конференциях и семинарах: II конференции молодых ученых СПбГУ ИТМО (2005 г.) — XXXIII, XXXV, XXXVI научных учебно-методических конференциях СПбГУ ИТМО «Достижения ученых, аспирантов и студентов СПбГУ ИТМО в науке и образовании» (2003, 2005, 2006 гг.) — «Телематика-2003», «Телематика-2004», «Телематика-2005», «Телематика-2006», «Телематика-2007» (СПб.) — на семинаре «Автоматное программирование» в рамках международной конференции «International Computer Symposium in Russia (CSR 2006)» (ПОМИ им. Стеклова, 2006 г.) — на конференциях «Software Engineering Conference in Russia» — SECR 2005 (Москва), «The International Scientific Conference «110-Anniversary of Radio Invention» (СП6ГЭТУ, IEEE, 2005 г.) — Второй Всероссийской научной конференции «Методы и средства обработки информации» (МГУ, 2005 г.) — Open Source Forum (М.: Форт-Росс, 2005 г.) — международной научно-технической конференции «Многопроцессорные вычислительные и управляющие системы» МВУС-2007 (Таганрог, 2007 г.) — научно-технической конференции «Научно-программное обеспечение в образовании и научных исследованиях» (СПб., 2008 г.).

Публикации. По теме диссертации опубликовано 23 печатные работы, в том числе в журналах из списка ВАК «Программирование», «Информационно-управляющие системы» и «Научно-технический вестник СПбГУ ИТМО», а также в журнале «Технология клиент-сервер» и материалах указанных конференций и семинаров.

Свидетельства об официальной регистрации программ для ЭВМ. На инструментальное средство, разработанное в рамках диссертации, получены свидетельства: «Ядро автоматного программирования».

2 006 613 249 от 14.09.2006, «Встраиваемый модуль автоматного программирования для среды разработки Eclipse» № 2 006 613 817 от 7.11.2006.

Структура диссертации. Диссертация изложена на 152 страницах и состоит из введения, пяти глав и заключения.

Список литературы

содержит 114 наименований. Работа иллюстрирована 59 рисунками и содержит три таблицы.

Выводы по главе 5.

1. При разработки системы автоматического завершения ввода в инструментального для инструментального средства итМо<�Л использовано само это средство — применен так называемый «метод раскрутки».

2. Разработанные методы и инструментальное средство успешно применены для выполнения студенческих проектов по курсу.

Organic Circular! i Hierarchic Orthogonal j Tree P.

• nerlfa') 4. p nextCb' ntjffb') -Гь e nev1(s)[*lst] end.

• nd[else] yFiles Evaluation Version je norj I ok J.

Автоматное программирование" на кафедре «Компьютерных технологий» СПбГУ ИТМО.

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

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

ЗАКЛЮЧЕНИЕ

.

В настоящей работе разработан метод проектирования объектно-ориентированных программ с явным выделением состояний. В рамках этого метода модель программы предлагается строить с помощью двух иМЬ-диаграмм — диаграмм классов и состояний. Разработанный метод апробирован при создании ряда приложений и показал свою эффективность. Он позволяет:

• сократить объем ручного программирования;

• при наличии библиотеки источников событий и объектов управления для определенной предметной области, полностью отказаться от ручного программирования;

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

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

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

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

Исходные тексты, документация и примеры использования программного пакета JniMod представлены на сайте http://unimod.sourceforge.net. За все время существования проекта было произведено более 45 000 скачиваний.

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

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

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

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