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

На правах рукописи | 00344 голи

Гуров Вадим Сергеевич

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

Специальность 05 13 11 Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата технических наук

0 2

0 ИТ 2008

Санкт-Петербург 2008

003447830

Работа выполнена в Санкт-Петербургском государственном университете информационных технологий, механики и оптики

Научный руководитель

Официальные оппоненты

доктор технических наук, профессор Шалыто Анатолий Абрамович

доктор технических наук, профессор Тропченко Александр Ювенальевич

кандидат физ -мат наук, доцент Новиков Федор Александрович

Ведущая организация

Санкт-Петербургский государственный электротехнический университет «ЛЭТИ»

Защита диссертации состоится «22» октября 2008 года в 14 часов на заседании диссертационного совета Д 212 227 06 при Санкт-Петербургском государственном университете информационных технологий, механики и оптики, 197101, Санкт-Петербург, ул Кронверкский 49, СПбГУ Ш МО

С диссертацией можно ознакомиться в библиотеке СПбГУ ИТМО

Автореферат разослан 19 сентября 2008 г

Ученый секретарь ( до^ Оур Ддлл/ ^ Тарлыков Владимир Алексеевич

СоветаД212 227 06, доктор технических наук, профессор

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Свидетельства об официальной регистрации программ для ЭВМ На инструментальное средство, разработанное в рамках диссертации, получены свидетельства «Ядро автоматного программирования» №2006613249 от 14 СЧ 2006, «Встраиваемый модуль автоматного программирования для среды разработки bchpse» №2006613817 от 7 И 2006 "

Структура диссертации Диссертация изложена на 152 страницах и состоит из введения, пяти глав и заключения Список литературы содержит 114 наименований Работа иллюстрирована 59 рисунками и содержит три таблицы

Содержание работы

Во Еведеняи обо; новывается ахлуальность темы диссертационной ¡-абога, описываются цель и задачи исследования Формулируются положения, ъыносичпе ча защиту

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

В чогле,аее время для повышенля уровня абстракции средств разработки программ развевается тякое направтснне программной инженерии как * Архитектура управгтсдт моделями» (Madd-Dmcn 4rchitecture, MDA) При применении MDA модели программных сио-ем представляются с помощью «Унифицированного языка моделирования» (Unified Modehng Language, UML) Если в течение ряда лег это* жык использовался только для представления моделей, то в последнее Еремя все большую популярность приобретает идея исполняемого UML

Моделирование динамических аспектов программ на языке UML затруднено в связи с отсутствием в стандарте на этот язык формального и однозначного описания правил интерпретации (операционной семантики) поведенческих диаграмм Кроме того, ни в одном из методов проектирования объектно-ориентированных систем, «внятно» не сказано, как связывать статические диаграммы с динамическими

Широким классом программных систем являются реактивные системы - системы, выполняющие определенные действия в ответ на внешние события В работах Д Харела показано, что для моделирования таких систем хорошо подходит расширение диаграмм переходов конечных автоматов, названное «диаграммы состояний» (Statechart)

Для построения диаграмм состояний и генерации кода по ним создан ряд ияструментачьных средств, таких как, например, I-Logix Stalemate, XJTek AnyState, StateSoft ViewControl, SCOPE, MR Systems visualSTATE, The State Machine Compiler

Недостаток этих инструментов состоит в том, что они позволяют строить и реализовывать только поведепческую часть модели программы, а не программу в целом Это связано с отсутствием в данных инструментах диаграммы, отображающей в явном виде связи между конечными автоматами и объектами, поведение которых моделируется Отметим, что спецификация UML позволяет задавать подобные связи с помощью диаграммы классов, однако ни в одной известной методологии не описано, как это делать Указанпый недостаток устранен в ¿ЖШГЛ-технологии, которая вводит в процесс проектирования диаграмму связей автомата для описания его интерфейса (входных и выходных воздействий)

В настоящей работе предлагается метод на основе SWITCH-тешолотя и UML-нотации, позволяющий строить единую формальную модель программ При этом диаграмма связей автомата представляется в виде t/AiL-диаграммы классов

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

Предлагается, сохранив автоматный подход, использовать UML-нотацию при построении диаграмм в рамках SWITCH-техиолотш, в которой программы строятся так же, как проводится автоматизация технологических процессов При этом, используя нотацию UML-дваграмм классов, строятся схемы связей автомагов, которые определяют их интерфейс, а графы переходов создаются с помощью дотации C/Affi-диаграммы состояний При наличии нескольких автоматов их схема взаимодействия не строится, а все они изображаются на диаграмме классов Эта диаграмма (как схема связей) и диаграммы состояний образуют предлагаемый графический язык для описания структуры и динамики программ

Для проектирования программ на основе этого язьша предлагается следующий

метод

1 На основе анализа предметной области в виде ¡/А/Ь-диаграммы классов разрабатывается копцептуальпая модель системы, определяющая сущности и отношения между ними

2 В отличие от традиционных для объектно-ориентированного программирования подходов, из числа сущностей выделяются источники событий, объекты управления и автоматы Источники событий активны - они по собственной инициативе воздействуют на автоматы Объекты управления пассивны - они выполняют действия, которые вызываются автоматами Объекты управления также могут формировать значения входных перемятых для автоматов Автоматы активируются источниками событий и па основании значений входных переменпых и текущих состояний воздействуют на объекты управления, переходя в новые состояния

3 Используя нотацию диаграммы классов, строится схема связей автоматов, которая задает интерфейс каждого их них На этой схеме слева изображаются источники событий, в центре - автоматы, а справа - объекты управления Источники событий с помощью ШЛ-ассоциаций связываются с автоматами, которым они поставляют события Автоматы связываются с объектами, которыми они управляют, а также с другими автоматами, которые они вызывают или которые вложены в их состояния

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

5 Каждый объект управления содержит два типа методов, реализующих входные переменные (х]) и выходные воздействия (гк) При этом отметим, что объект управления инкапсулирует вычислительные состояния системы, которые обычно явно не выделяются из-за большого их числа

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

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

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

9 Каждый автомат имеет одно начальное и произвольное число конечных состояний

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

11 Все сложные состояния неустойчивы, а все простые, за исключением начального -устойчивы При наличии сложных состояний в автомате, появление события может привести к выполнению более одного перехода. Это происходит в связи с тем, что, как отмечено выше, сложное состояние является неустойчивым, и автомат выполняет переходы до тех пор, пока не достигнет первого из простых (устойчивых) состояний

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

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

Предлагаемый метод позволяет выполнить проектирование программы в

целом

На рис 1 приведен пример схемы связей автомата, а на рис 2 - его граф переходов

у-- у. - —

У Е21: String - "е21* {dent loosedln) У £22; String = е22' {Client togged out} if E23: String - "e23" (Replica) У E24: String = e24" (Users)

y El: String - *el" {Send button pressed) y E2: String - *e2" (Connect button press, ElflO: String - *elOO" {Window dosed)

-T-v-y-T-

g3 Connects tyjff Alj

й

© zl! void (Connect to server) © zh void (Disconnect from server) © z3: void (Send replica to server)

© z3: void (Update users Bst)

© z4: void (Add replica to dialog panel)

©z5: void {(-txiate status line and connect button to connected)

© z6: void {Update status line and connect button to c£s connected)

-T"

© xL' boolean {Is con fig initialization success fU)

"a \ © *controfiedobjerf£ ^,

i • > 1 1 J ' " ' _ ^ " '

Рис. 1. Пример схемы связей автомата

Рис. 2. Пример графа переходов автомата

Синтаксис созданного 1рафического языка автоматного программирования основан на Ш/Х-нотации. При этом предлагается использовать следующие элементы £/М£-диаграммы состояний: начальное, нормальное и конечное состояния и переходы между ними. Состояния на диаграмме могут быть простыми и сложными. Если в нормальное состояние вложено другое состояние, то оно называется сложным. В противном случае состояние простое. Наличие дуги, исходящей из сложного состояния, заменяет однотипные дуги из каждого вложенного состояния. Каждое сложное состояние содержит одно начальное состояние, а каждая диаграмма содержит одно головное состояние - сложное состояние, содержащее все остальные состояния. Для нормальных состояний могут быть определены действия при входе в состояние и вложенные

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

Пометка на переходе состоит из события, инициирующего переход, условия и списка действий На переходе может быть использовано либо событие, определенное в одном из источников, связанных с данным автоматом, либо символ «*», означающий любое событие В качестве переменных в условиях на переходах, используются имена методов объектов управления, связанных с автоматом

С/А£[.-состояния с параллельными регионами не поддерживаются Это связано с тем, что проектирование объектов с одним потоком управления является достаточно простым, а для отражения параллелизма следует использовать несколько параллельно исполняемых автоматов

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

Для модели системы, построенной описанным выше образом и состоящей из статической и динамической частей, задается операционная семантика

1 При запуске модели инициализируются все источники событий и объекты управления После этого источники событий начинают воздействовать на связанные с ними автоматы

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

3 При получении события автомат выбирает все исходящие из текущего состояния переходы, помеченные символом этого события

4 Автомат перебирает выбранные переходы и вычисляет логические формулы, записанные на них, до тех пор, пока не найдет формулу со значением true

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

6 Если среди выходных воздействий встречается вызываемый автомат, то он вызывается с соответствующим событием

7 Если переход не найден, то автомат продолжает поиск перехода у родительского состояния - состояния, в которое вложено текущее состояние

8 При переходе в конечное состояние автомат останавливает все источники событий На этом работа системы завершается

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

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

• тестирование,

• имитационное моделирование,

• дедуктивный анализ,

• верификация на модели

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

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

Для проверки полноты и непротиворечивости множества переходов, для каждой вершины необходимо решать задачу проверки тождественного равенства единице или нулю логической формулы В данном случае логической формулой являются логические формулы, в которых используются следующие бинарные отношения '>', '<', '>=', '<=', '=', V При этом в качестве левого аргумента должна стоять целочислепная переменная, а справа - целочисленная константа

Для решения указанной задачи можно использовать два подхода

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

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

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

Алгоритм минимизации реализован для грамматики охранных условий Построение синтаксического анализатора для данной грамматики осуществлялось с помощью библиотеки АЫТЬК, позволяющей автоматически по заданной ¿¿(^-грамматике строить транслятор входного потока в синтаксическое дерево разбора Дерево, полученное в результате трансляции, можно использовать для вычисления значений формул во время выполнения программы, а также трансформировать в другое дерево

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

1 Приведение формулы к дизъюнктивной нормальной форме (ДНФ)

2 Упрощение термов ДНФ

3 Нахождение интервалов целочисленных переменных, входящих в терм, при которых он не обращается в ложь

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

Дня приведения синтаксического дерева к дереву, соответствующему ДНФ, необходимо и достаточно удовлетворить следующие условия

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

• ни один узел, соответствующий конъюнкции, не должен быть предком по отношению к узлам, соответствующим дизъюнкции

Предлагаемая процедура проверки полноты систем переходов состоит из следующих этапов

1 Построение дизъюнкции формул условий на переходах

2 Оптимизация термов в дизъюнкции

3 Приведение к ДНФ отрицания формулы, полученной на шаге (2)

4 Оптимизация термов в формуле, полученной на шаге (3)

5 Равенство нулю результирующей формулы означает полноту системы формул

Проверка непротиворечивости выполняется аналогично

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

• источники событий - инициируют работу системы,

• объекты управления - выполняют действия и формируют входные переменные,

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

Верификация на модели автоматных программ состоит в проверке того, чгго управляющая система работает корректно, что определяется выполнением темпоральных утверждений вида «если произошло событие el, то когда-нибудь будет вызвано действие zl» или «если всегда неверно xl (xl всегда false), то автомаг никогда не попадет в состояние s2» Утверждения, которые требуется проверить, называют требованиями, а их совокупность — спецификацией В том случае, если система автоматов удовлетворяет -спецификации, считается, что верификация завершена успешно Если хотя бы одно из требований не выполняется, то существует последовательность действий, которая приводит к нарушению этого требования Такая последовательность называется контрпример

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

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

Традиционно при верификации программы для нее строится модель Крите -неявно заданный граф атомарных (вычислительных) состояний и переходов между ними Модель Крипке является подробной схемой работы программы

Требования к программе формулируются в виде формулы темпоральной логики, причем в данном случае используется LTL (Linear Temporal Logic)

¿7Х-формула преобразуется в автомат Бюхи - конечный автомат над бесконечными словами Переходы автомата Бюхи помечены предикатами из исходной ¿TZ-формулы Поскольку задача верификатора - найти контрпример, если он существует, автомат Бюхи строится для отрицания 171-формулы

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

двойного поиска в глубину (модифицированный алгоритма Тирьяна), который находит допускающую последоватглыюсть предикатов Если эта последовательность существует, то она является контрпримером

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

В верификаторе Bogor явно не строятся модель Крипке, автомат Бюхи для меде та Крипке и его пересечение с автоматом Бюхи для ¿ТХ-формулы Верифицируемая программа записывается на входном язьпсе верификатора Это позволяет верификатору выделять в программе элементарные действия, поскольку в семантике этого языка определено, какие действия совершаются атомарно, как откатывать назад эти действия, возвращая систему в предыдущее состояние, как вычислять состояния объектов (переменных) и какие операторы порождают недетерминированность При этом верификатору Bogor необходимо выполнять следующие действия

1 Вычислять глобальное состояние программы

2 Совершать элементарный шаг работы программы - переход программы из одного глобального состояния в другое без посещения иных глобальных состояниГ'

3 Откатывать назад элементарные шаги работы программы

4 В каждом состоянии определять возможные дальнейшие элементарные шаги

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

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

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

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

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

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

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

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

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

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

moivt верифицироваться с помощью дедуктивны^ методов, основанных in проверке быпо тнеьнл пред- н постусловий

В четверток главе описана реализация ииструменгальни'-о средстзл UruMod дчя поддерАхн ра^работанш го графического языка и методов проектирования и верификации, изложенных в предыдущих главах Она выполнена на языке Java в виде плагина дня среды разработки Eclipse

UmMoa позволяет создавать и редактировать {/Mi-диаграммы классов и состояний, которые соответствуют схемам связей и графам переходов автоматов

При проектировании программ с использованием этого средства ее структура задается схемой связей в виде UML-диаграммы классов, а поведение - системой взаимодействующих автоматов, заданных в виде набора (/¿¿¿-диаграмм состояний Источники событий и объекты управления реализуются вручную на цетевом языке программирования

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

Для обеспечения эффективности процесса разработки в инструмент ~д,ьоч средстве UrnMod также реализована следующая функциональность

• подсветка синтаксических и семантических ошибок,

• завершение ввода и исправление ошибох ввода при педактиповапии пометок на переходах диаграмм состояний,

• запуск модели на исполнение,

• интерактивпая отладка модели в терминах автомата

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

UniModявляется проектом с открытым исходным кодом, который опубликован на сайте проекта bttp //unipiod bf net На момент написания диссертации было выпушено более 30 версий проекта и осуществлено ботее 40000 скачиваний Ссылки на Un ffod можно найти на десятках сайтов, посвященных автоматизации программирования

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

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

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

«в компании eVelopers для разработал интернет-приложегай а мобгльшлс

приложений,

• в компания JetBrams гри разработче системы мета-программ чр^зтния Me7.i

Programming Syite.n (MPS),

• в учеСш. si процессе СПСГУ ИГМО при разработке lypiobbix проектов Ошпгем Э1Ч облити вне фенил более подробно

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

Технология основывается на том, чтобы для заданной ¿¿(^-грамматике построить конечный автомат Мили, который будет синтаксическим анализатором Автомат должен реагировать на события, поставляемые ему лексическим анализатором Каждому событию

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

Внедрение в промышленное программирование В качестве примера применения инструментального средства UmMod в компании eVelopers в диссертации описан процесс разработки автоответчика для мобильного телефона Nokia 6600 На данном устройстве установлена операционная система Symbian, а разработка приложений выполняется на языке С++

Для этого языка созданы шаблоны для генерации кода, что позволило применять пакет UmMod при использовании языка С++,как целевого языка программирования Интерпретационный подход на языке С++ не реализован, так как для мобильных устройств требуется высокое быстродействие, обеспечиваемое при компиляции

Разработан метод формального и изоморфного перехода от спецификации к текстам программ на языке С++ Формальность перехода позволяет для одного 1рафа переходов использовать его в качестве полного теста для сертификации построенной программы, а изоморфность с графом переходов - проверять программу сверкой ее текста со спецификацией

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

Текстовый язык автоматного программирования Инструментальное средство UmMod, наряду с перечисленными выше достоинствами, обладает и недостатками

• ввод диаграмм состояний с помощью графического редактора весьма трудоемок,

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

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

Для устранения перечисленных недостатков был предложен новый подход к разработке автоматных программ и применению автоматов в объектно-ориентированных системах В рамках этого подхода предлагается использовать систему метапрограммирования JetBrains Meta Programming Systerr (MPS), которая позволяет создавать проблемно-ориентированные языки (Domain Specific Language - DSL) С помощью MPS созданы два варианта текстового языка для автоматного программирования Первый язык выполнен в виде расширения языка Java, а второй -самостоятельным языком Эти языки позволяют описывать состояния и логику переходов автоматов, а также события, обрабатываемые автоматами При этом также как и в инструментальном средстве UmMod, функции входных и выходных переменных реализуются на другом языке программирования, таком как Java или С++

Внедрение в учебный процесс С помощью инструментального средства UmMod на кафедре «Компьютерные технологии» СПбГУ ИТМО реализовано около 30 студенческих проектов, в которых эмулировалась работа банкоматов, стиральных машин, турникетов в метро, автомобильной сигнализации и т д Работы опубликованы на сайте http //is lfino ru/unimod-proiects

Заключение

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

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

2 Разработан графический язык программирования на основе ¡УЛ/Х-нотации для поддержки указанного метода

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

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

5 Полученные результаты внедрены в практику разработки программного обеспечения и в учебный процесс в СПбГУ ИТМО

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

Список публикаций

1 Гуров В С, Нарвский А С, Шалыто А А Автоматизация проектирования событийных объектно-ориентированных программ с явным выделением состояний // Труды X Всероссийской научно-методической конференции «Телематика-2003» СПбГИТМО (ТУ) 2003

2 Гуров В С, Мазин М А, Нарвский А С, Шалыто A A UML SWITCH-технология Eclipse//Информационно-управляющие системы 2004 №6, с 12-17

3 Гуров В С, Нарвский А С, Шалыто A A ICQ и Автоматы // Технология клиент-сервер 2004 №3,с 3-11

4 Гуров В С, Мазин М А, Нарвский А С, Шалыто А А Разработка средств автоматизации построения объектно-ориентированных программ с явным выделением состояний // Научно-технический вестник СПбГУ ИТМО Выл 16 Актуальные проблемы современных оптико-информационных систем и технологий 2004,с 88-100

5 Гуров В С, Мазин М А, Шалыто A A UNIMOD - программный пакет для разработки объектно-ориентированных приложений на основе автоматного подхода //Труды XI Всероссийской научно-методической конференции «Телематика-2004» СПбГУ ИТМО Т 1, с 189-191

6 Горшкова Е А, Новиков Б А, Белов Д Д, Гуров В С, Спиридонов С В Моделирование контроллера Web-приложений с использованием UML //Программирование 2005 № 1, с 44-51

7 Гуров В С, Мазин М А, Нарвский А С, Шалыто A A UmMod Метод и средство разработки реактивных объектно- ориентированных прогр<тм l. явьым вьщелением состояний /Труды Второй Всероссийской научной конференции «Методы и средства обработки информации» МГУ 2005, с 361-366

8 Гуров В С, Мазин М А Создание системы автоматического завершения ввода с использованием пакета UmMod /Вестник II межвузовской конференции молодых ученых Т1 СПбГУ ИТМО 2005, с 73-87

9 Гуров В С, Мазин М А, Шалыто А А Операционная семантика UML-диаграмм состояний в программном пакете UmMod //Труды XII Всероссийской научно-методической конференции «Телематика-2005» СПбГУ ИТМО Т 1, с 74-76

10 Гуров В С, Мазин М А, Нарвский А С, Шалыто А А Исполняемый UML Проект UmMod /Software Engineering Conference (Russia) - 2005 M РУССОФТ Abstracts, с 12-13

11 Gurov V S, Mazin M A, Narvsky A S, Shalyto A A UmMod Method and Development of Reactive Object-Oriented Programs with Explicit States Emphasis

/Proceedmgs 2005 of St Petersburg IEEE Chapters International Conference «110 Anniversary of Radio Invention» SPb ETU «LETI» 2005, pp 106-110

12 Гуров В С, Мазин М А, Нарвский А С, Парфенов В Г, Шалыто A A UniMod -инструментальное средство для поддержки автоматного программирования //Материалы X Всероссийской конференции по проблемам науки и высшей школы «Фундаментальные исследования в технических университетах» СПбГ ПУ 2006, с 481-488

13 Гуров В С, Мазин М А, Парфенов В Г Графический отладчик UML-диаграмм состояний в программном пакете UniMod //Труды XIII Всероссийской научно-технической конференции «Телематика-2006» СПбГУИТМО 2006, с 106-110

14 Гуров В С, Мазин М А, Нарвский А С, Шалыто А А Инструментальное средство для поддержки автоматного программирования //Рабочий семинар «Наукоемкое программное обеспечение» на шестой международной конференции «Перспективы систем информатики» Новосибирск Институт проблем информагаки имени А П Ершова. СО РАН 2006, с 52-54

15 Гуров В С, Мазин М А, Нарвский А С, Шалыто A A UniMod -инструментальное средство для автоматного программирования //Материалы третьей международной конференции по проблемам управления М Институт проблем управления 2006, с 224-227

16 Гуров В С, Мазин М А, Шалыто A A UniMod - Инструментальное средство для автоматного программирования // Фундаментальные и прикладные исследования информационных систем и технологий Научно-технический вестник СПбГУ ИТМО Вып 30 2006, с 32-44

17 Гуров В С, Мазин М А, Нарвский А С, Шалыто А А Инструментальное средство для поддержки автоматного программирования //Программирование 2007 №6, с 65-80

18 Гуров В С, Мазин М А, Зубок Д А, Парфенов В Г, Шалыто А А Два подхода к созданию программ с использованием инструментального средства UniMod //Труды XIV Всероссийской научно-методической конференции «Телематика-2007» СПбГУ ИТМО, 2007

19 Гуров В С, Шалыто А А, Яминов Б Р Технология верификации автоматных моделей программ без их трансляции во входной язык верификатора //Материалы международной научно-технической конференции «Многопроцессорные вычислительные и управляющие системы» (МВУС-2007) Т 1, с 198-203

20 Гуров В С, Мазин М А, Шалыто А А Текстовый язык автоматного программирования //Труды научной конференции «Компьютерные науки и технологии» Саратов СГУ 2007, с 66-69

21 Гуров В С, Мазин М А, Шалыто А А Текстовый язык автоматного программирования //Фундаментальные и прикладные исследования информационных систем и технологий Научно-технический вестник СПбГУ ИТМО Вып 42 2007, с 29-32

22 Гуров В С, Мазин М А, Шалыто А А Автоматическое завершение ввода условий в диаграммах состояний //Информационно-управляющие системы 2008 № 1, с 24-33

23 Гуров В С, Яминов Б Р Технология верификации автоматных моделей программ без их трансляции во входной язык верификатора /Материалы научно-технической конференции «Научное программное обеспечение в образовании и научных исследованиях» СПбГПУ 2008, с 36-40

Тиражирование и брошюровка выполнены в центре «Университетские телекоммуникации» Санкт-Петербург, Саблинскаяул 14, тел (812)233-4669 Тираж 100 экз

ВВЕДЕНИЕ.

ГЛАВА 1. ТЕХНОЛОГИИ ПРОЕКТИРОВАНИЯ И РАЗРАБОТКИ ОБЪЕКТНО-ОРИЕНТИРОВАННЫХ ПРОГРАММ.

1.1. Реактивные системы.

1.2. Классификация автоматных подходов.

1.3. Гибридные автоматы.

1.4. Автоматное программирование встраиваемых систем.

1.5. Использование автоматного подхода при реализации прикладных программ.

1.6. Программные продукты для графического моделирования конечных автоматов.

1.6.1. Finite State Machine Editor.

1.6.2. Среда разработки Флора.

1.6.3. XJTek AnyState.

1.6.4. IAR Systems visualSTATE.

1.6.5. Telelogic Tau2.

1.6.6. Borland Together Architect.

1.7. Исполняемый UML.

1.8. SWITCH-технология.

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

ГЛАВА 2. РАЗРАБОТКА МЕТОДА ПОСТРОЕНИЯ ОБЪЕКТНО-ОРИЕНТИРОВАННЫХ ПРОГРАММ С ИСПОЛЬЗОВАНИЕМ АВТОМАТНОГО ПОДХОДА.

2.1. Исполняемый графический язык автоматного программирования и метод построения программ на его основе.

2.2. Синтаксис графического языка.

2.3. Операционная семантика графического языка.

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

ГЛАВА 3. ВЕРИФИКАЦИЯ МОДЕЛЕЙ АВТОМАТНЫХ ПРОГРАММ.

3.1. Дедуктивный анализ автоматных моделей.

3.2. Верификация на модели.

3.2.1. Метод верификации.

3.2.2. Сравнение метода эмуляции с методом верификации автоматных программ, известным из литературы.

3.2.3. Применение верификатора.

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

ГЛАВА 4. ИНСТРУМЕНТАЛЬНОЕ СРЕДСТВО ДЛЯ ПОДДЕРЖКИ АВТОМАТНОГО ПРОГРАММИРОВАНИЯ UNIMOD.

4.1. Интерпретация.

4.2. Компиляция.

4.3. Реализация редактора диаграмм на платформе Eclipse.

4.3.1. Завершение ввода и исправление ошибок ввода.

4.3.2. Форматирование.

4.3.3. Исполнение модели.

4.4. Отладка модели.

4.4.1. Статическая модель отладчика.

4.4.2. Динамическая модель отладчика.

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

ГЛАВА 5. ВНЕДРЕНИЕ ПРЕДЛОЖЕННЫХ РЕЗУЛЬТАТОВ РАБОТЫ В

ПРАКТИКУ ПРОЕКТИРОВАНИЯ.

5.1. Создание системы автоматического завершения ввода.

5.1.1. Описание предлагаемой технологии.

5.1.2. Построение диаграммы переходов синтаксического анализатора

5.1.3. Удаление правой рекурсии.

5.1.4. Удаление немотивированных переходов.

5.1.5. Подстановка диаграмм переходов друг в друга.

5.1.6. Удаление срединной рекурсии.

5.1.7. Модель разрабатываемой системы.

5.1.8. Восстановление после ошибок.

5.1.9. Получение множества строк для автоматического завершения ввода

5.1.10. Пример работы системы.

5.2. Внедрение в учебном процессе.

5.3. Создание мобильного приложения.

5.3.1. Постановка задачи.

5.3.2. Статическая модель системы.

5.3.3. Динамическая модель системы.

5.3.4. Создание кода.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Перечисленные результаты получены в ходе выполнения в СПбГУ ИТМО научно-исследовательских и опытно-конструкторских работ по темам: «Разработка технологии создания программного обеспечения систем управления на основе автоматного подхода» (проводится по заказу Минобрнауки РФ с 2000 г. по настоящее время), «Разработка технологии автоматного программирования» (проводилась в 2002-2003 гг. по гранту Российского фонда фундаментальных исследований № 02-07-90114), «Разработка технологии объектно-ориентированного программирования с явным выделением состояний» (проводилась в 2005-2006 гг. по гранту Российского фонда фундаментальных исследований № 05-07-90011), «Технология автоматного программирования: применение и инструментальные средства» (государственный контракт, который выполнялся в 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 печатные работы, в том числе в журналах из списка ВАК «Программирование», «Информационно-управляющие системы» и «Научно-технический вестник СПбГУ ИТМО», а также в журнале «Технология клиент-сервер» и материалах указанных конференций и семинаров.

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

2006613249 от 14.09.2006, «Встраиваемый модуль автоматного программирования для среды разработки Eclipse» №2006613817 от 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. За все время существования проекта было произведено более 45000 скачиваний.

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

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

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

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

1. Соммервилл И. Инженерия программного обеспечения. М.: Вильяме, 2002.

2. Грехем И. Объектно-ориентированные методы. Принципы и практика. М.: Вильяме, 2004.

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

4. Ларман К. Применение UML и шаблонов проектирования. М.: Вильяме, 2001.

5. Коуд П., Норт Д., Мейфмлд М. Объектные модели. Стратегии, шаблоны и приложения. М.: Лори, 1999.

6. Harel D., Politi М. Modelling Reactive Systems with Statecharts. NY: McGraw-Hill, 1998.

7. Harel D. Statecharts: A Visual Formalizm for Complex Systems //Science of Computer Programming. 1987. № 8, pp. 231-274.

8. Harel D. et al. STATEMATE: A Working Environment for the Development of Complex Reactive Systems //IEEE Transactions on Software Engineering. 1990. №4, pp. 234-252.http://csdl.computer.org/comp/trans/ts/1990/04/e0403abs.htm

9. Кузнецов С. Обещания и просчеты UML 2.0 //Открытые системы. 2006. № 2, с. 75-79.10. 1st European Conference on Model-Driven Software Engineering. Germany. 2003. http://www.agedis.de/conference/

10. International Workshop «e-Business and Model Based in System Design». IBM EE/A. SPb ETU, 2004.

11. OMG Model Driven Architecture, http://www.omg.org/mda/

12. Frankel D. Model Driven Architecture: Applying MDA to Enterprise Computing. NJ: Wesley, 2003.

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

14. Mellor S., Balcer М. Executable UML: A Foundation for Model Driven Architecture. MA: Addison-Wesley, 2002.

15. Raistrick C., Francis P., Wright J. Model Driven Architecture with Executable UML. Cambridge University Press, 2004.

16. Wikipedia. Finite state machine. http://en.wikipedia.org/wiki/Finitestate machine#Externallinks

17. Sun Studio Enpterprise. http://developers.sun.com/prodtech/iavatools/jsenterprise/reference/techart/wh atis.html

18. Jacobson I. Four Macro Trends in Software Development Y2004. http://www.ivarjacobson.com/postnuke/html/modules.php?op=modload&nam e=UpDownload&file=index&req=getit&lid-9ч

19. I-Logix Statemate. http://ilogix.com/sublevel.aspx?id=74

20. XJTek Any State, http://www.xitek.com/anystates/ ,

21. StateSoft ViewControl. http://www.statesoft.ie/products.html

22. SCOPE, http://www.itu.dk/~wasowski/proiects/scope/

23. IAR Systems visualSTATE. http://www.iar.com/pl 014/pl014 eng.php

24. The State Machine Compiler, http://smc.sourceforge.net/

25. Jia X. et al. Using ZOOM Approach to Support MDD. http://se.cs.depaul.edu/ise/zoom/papers/zoom/SERP ZOOM.pdf

26. Гамма Э., Хелм P., Джонсон P., Влиссидес Дж. Приемы объектно-ориентированного проектирования. Паттерны проектирования. СПб.: Питер, 2001.

27. Шамгунов Н. Н., Корнеев Г. А., Шалыто A. A. State Machine новый паттерн объетно-ориентированного проектирования //Информационно-управляющие системы. 2004. № 5, с. 32-36. http://is.ifmo.ru/works/pattern/

28. The Hybrid Systems Project, http://control.ee.ethz.ch/~hybrid/

29. Ferrari-Trecate G. at el. Mixed Logic Dynamical Model of a Hydroelectric Power Plant.http://control.ee.ethz.ch/research/publications/publications.msql?banner=hybr id&action-Showdetails&id=859

30. Бенъкович E., Колесов Ю., Сениченков Ю. Практическое моделирование динамических систем. СПб.: БХВ, 2002.

31. Model Vision Studium, http://www.exponenta.ru/soft/others/mvs/mvs.asp

32. XJTek Any Logic, http://www.xitek.com/anylogic/

33. Беляев А. В., СуясовД. К, Шалыто А. А. Компьютерная игра космонавт. Проектирование и реализация //Компьютерные инструменты в образовании. 2004. № 4, с. 75-84.http://is.ifhio.ru/works/ cosmo article.pdf

34. Шалыто А., Туккелъ Н., Шамгунов Н. Ханойские башни и автоматы //Программист. 2002. № 8, с. 82-90. http://is.ifmo.ru/works/hanoy/

35. Шалыто А., Туккелъ Н. От тьюрингова программирования к автоматному //Мир ПК. 2002. № 2, с. 144-149.http ://is. i fmo.ru/ works/turin g /

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

37. Xilinx StateCAD. http://www.xilinx.com/xlnx/xebiz/designResources/ip product details.jsp?sG lobalNavPick=PRODUCTS&sSecondarvNavPick=Design+Tools&kev=dr dtstatemachine

38. Altera Quartus //.http://www.altera.com/products/software/sfw-index.isp

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

40. State Logic. http://www.geindustrial.com/cwc/products?pnlid=2&id=sl

41. I-Logix Rhapsody. http://www.ilogix.com/rhapsody/rhapsQdy.cfm

42. Mathworks State/low. http://www.mathworks.com/products/stateflow/

43. Шалыто А. А., Туккелъ H. И. SWITCH-технология автоматный подход к созданию программного обеспечения «реактивных» систем. //Программирование. 2001. № 5, с. 42-54.http://is.ifmo.ru/works/ avtomatnij podhod k sozdaniju programmnogo ob espechenija.divu

44. Gibson D. Finite State Machines. Making simple work of complex functions. http://www.microconsultants.com/tips/fsm/fsmarticl.pdf

45. A Framework for Hardware-Software Co-Design of Embedded Systems. http://www-cad.eecs.berkeley.edu/~polis/

46. VIS (Verification Interacting with Synthesis). http://www-cad.eecs.berkeley.edu/Respep/Research/vis/index.html

47. Ахо А., Сети P., Ульман Д. Компиляторы: принципы, технологии и инструменты. М.: Вильяме, 2001.

48. Хантер Р. Основные концепции компиляторов. М.: Вильяме. 2002.

49. Кормен Т., Лайзерсон Ч., Ривест Р. Алгоритмы. Построение и анализ. М.: МЦМНО, 2000.

50. Корнеев Г. А., Шамгунов Н. Н., Шалыто А. А. Обход деревьев на основе автоматного подхода //Компьютерные инструменты в образовании. 2004. № 3, с. 32-37. http://is.ifmo.ru/works/traverse/

51. Шалыто А. А., Наумов JI. А. Методы объектно-ориентированной реализации реактивных агентов на основе конечных автоматов //Искусственный интеллект. 2004. № 4, с. 756-762.

52. Werken Blissed. Java State-Machine Framework, http://blissed.werken.com/54. boost: :fsm. С++ library for finite state machines. http://boost-sandbox.sourceforge.net/fsm.zip.

53. Ninni FSM Generator, http://nunnifsmgen.nunnisoft.ch/en/home. isp

54. Finite State Machine generating software. http ://fsmgenerator. sourceforge. net/

55. Finite State Machine (FSM). http://finsm.sourceforge.net/

56. The State Machine Compiler, http://smc.sourceforge.net/

57. Duval P-Y. et al. Evaluation of CHSM (Concurrent Hierarchical State Machine) language system. http://atddoc.cern.ch/Atlas/Notes/Q 12/NoteO 121 .html

58. Open Source Page Flow Written in Java. http://www.manageability.org/blog/stuff/open-source-statemachine-for-user-interfaces-written-in-java

59. StateSoft ViewControl. http://www.statesoft.ie/products.html

60. Java 2 Platform, Enterprise Edition (J2EE). http://iava.sun.com/i2ee/index.isp

61. Gurevich Y. Evolving Algebra 1993: Lipari Guide in «Specification and Validation Methods». Oxford University Press, 1995.

62. AsmL for Microsoft .NET. http://research.microsoft.com/fse/asml/doc/StartHere.htmls

63. Карпов Ю. Г. Теория автоматов. СПб.: Питер, 2002.

64. Finite State Kernel Creator, http://fskc.sourceforge.net/

65. UML Products By Company. http://www.objectsbydesign.com/tools/umltools byCompany.html

66. Терехов A. H., Романовский К. Ю., Кознов Д. В. и др. REAL: Методология и CASE-средство разработки информационных систем и программного обеспечения //Программирование. 1999. № 3, с. 18-24.

67. Nucleus UML Suite, http://www.projtech.com/embedded/nuc modeling.html

68. UML Specification 1.5. http://www.omg.org/cgi-bin/apps/doc7formal/03-03-Ol.pdf

69. A Validation Toolset for UML. http://www.eecs.umich.edu/~wwshen/tool/tool.html

70. IBM ОСЬ Parser. ftp://ftp.software.ibm.com/soitware/websphere/awdtools/standards/ocl-parser-03.zip

71. Андреев H. Автоматическая верификация модели UML. СПб ГТУ, 2002. http://bicamp.aanet.ru/2003/papers/sectionIT/AndreevND.pdf

72. Maller-Pedersen В. Specification and Description Language. SDL + UML. //Telektronik. 2000. № 4, pp. 22-30.http://www.item.ntnu.no/fag/ttm4115/UMLandSDL/Telek4 2000%20SDL-UML.pdf

73. Douglas B. Real-Time UML: Developing Efficient Objects for Embedded Systems. MA: Addison-Wesley, 1998.

74. Гома X. UML. Проектирование систем реального времени, параллельных и распределенных приложений. М.: ДМК Пресс, 2002.

75. ITU-T. SDL combined with UML (Z. 109). Geneva. ITU-T, 2000.

76. Specification and Design Language (SDL). http://www.sdl-forum.org/SDL/index.htm

77. Шалыто А. А., Туккелъ H. И. Автоматы и танки //BYTE/Россия. 2003. № 2, с. 28-32. http://is.ifmo.ru/works/tanks new/

78. Visio2Switch. http://www.softcraft.ru/auto/switch/v2s.shtml

79. Finite State Machine Editor, http://fsme.sourceforge.net/

80. Ваганов С. Ускоритель разработки приложений //Открытые системы. 2004. № 6, с. 40-44.

81. Telelogic Таи2. http://www.telelogic.com/products/tau/tg2.cfm

82. Rambaugh J., Jacobson I., Booch G. The Unified Modeling Language Reference Manual. Addison-Wesley, 2005.

83. Borland Together Architect. http://www.borland.com/together/architect/index.html

84. Фаулер M. UML. Основы. СПб.: Символ-Плюс, 2004.

85. Фаулер М. Рефакторинг: улучшение существующего кода. СПб.: Символ-Плюс, 2002.

86. Riehle D., Fraleigh S., Bucka-Lassen D., Omorogbe N. The Architecture of a UML Virtual Machine / Proceedings of the 2001 Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA '01). ACM Press, 2001.

87. Matilda UML Virtual Machine, http://dssg.cs.umb.edu/projects/umlvm/

88. Carter K. iUML. http://www.kc.com/products/iuml/index.htm 1

89. Глушков B.M. Синтез цифровых автоматов. M.: Физматгиз, 1962.

90. MetaObject Facility Core Speification Version 2.0. http://www.omg.org/technology/documents/formal/MOF Core.htm

91. Гэри M., Джонсон Д. Вычислительные машины и труднорешаемые задачи. М.: Мир, 1982.

92. Верещагин Н., Шенъ А. Лекции по математической логике и теории алгоритмов. Часть 2. Языки и исчисления. М.: МЦНМО, 2000.

93. Parr Т. J., Quong R. W. ANTRL: A Predicated-LL(k) Parser Generator // Software Practice And Experience. 1995, №25(7), pp. 789-810.

94. Васильева К. А., Кузьмин E. В. Верификация автоматных программ с использованием LTL // Моделирование и анализ информационных систем. 2007. Т. 14. № 1, с. 3-14.

95. Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. М.: МЦНМО, 2002

96. Holzmann G. The Model Checker Spin. IEEE Trans, on Software Engineering, Vol. 2. 1997, No. 5, pp. 279-295.

97. Robby, Lhvyer M., Hatclijf J. Bogor: A Flexible Framework for Creating Software Model Checkers. TAIC PART 2006, pp 3-22.

98. Velocity. Java-based template engine. http://iakarta.apache.org/velocity/index.html

99. Fruchterman Т. M. J., Reingold E. M. Graph Drawing by Force Directed Placemen I I Software Practice and Experience. 1991. № 21(11), pp. 1129— 1164.

100. Java Debug Wire Protocol. http://iava.sun.eom/i2se/l.5.0/docs/guide/ipda/jdwp-spec.html104. Java Networking Features.http ://j ava. sun, com/j 2 se/1.5.0/docs/guide/net/index.html

101. Шалыто А. А., Штучкин А. А. Совместное использование теории построения компиляторов и SWITCH-технологии (на примере построения калькулятора). СПбГУ ИТМО. 2003. http :П\s .ifmo.ru/proj ects/calc/

102. Легалов А. И. Основы разработки трансляторов. Использование диаграмм Вирта для представления динамически порождаемых конечных автоматов, распознающих КС(1) грамматику. http://softcraft.ru/translat/lect/t08-04.shtml

103. Шалыто А. А., Туккелъ Н. И., Шамгунов Н. Н. Реализация рекурсивных алгоритмов на основе автоматного подхода. //Телекоммуникации и информатизация образования. 2002. № 5, с. 52-68. http://is.ifmo.ru/works/recurse/

104. Акимов О.Е. Дискретная математика: логика, группы, графы. М.: Лаборатория Базовых Знаний. 2003.

105. Harrison R. Symbian OS С++ for Mobile Phones. John Wiley & Sons, 2003.

106. Fowler M. Language Workbenches: The Killer-App for Domain Specific Languages? http://www.martinfowler.com/articles/languageWorkbench.html9 м1

107. Фаулер М. Языковой инструментарий: новая жизнь языков предметной области. http://www.maxkir.com/sd/languageWorkbenches.html)

108. Dmitriev S. Language Oriented Programming: The Next Programming Paradigm //onBoard. 2005. № 2. (Дмитриев С. Языково-ориентированное программирование: следующая парадигма//RSDN Magazine. 2005. № 5).

109. Ward М. Language Oriented Programming //Software Concepts and Tools. 1994. 15.

110. Luo Z. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, 1994.

111. Simonyi C. The Death of Computer Languages, the Birth of Intentional Programming /The Future of Software. Univ. of Newcastle upon Tyne, England, Dept. of Computing Science, 1995.

112. Kachelaev D., Khasanzyanov В., Yaminov В., Shalyto A. Instrumental Tool for Automata Based Software Development UniMod 2 /Proceeding of the Second Spring Young Researchers' Colloquium on Software Engineering. V. 1. SPbSU. 2008, pp. 55-58.