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

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

СТЕПАНОВ Олег Георгиевич

МЕТОДЫ РЕАЛИЗАЦИИ АВТОМАТНЫХ ОБЪЕКТНО-ОРИЕНТИРОВАННЫХ ПРОГРАММ

Специальность 05.13.11 - «Математическое обеспечение вычислительных машин, комплексов и компьютерных сетей»

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

1 О ДЕК 2009

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

003487924

Работа выполнена в Санкт-Петербургском государственном информационных технологий, механики и оптики (СПбГУ ИТМО)

университете

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

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

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

доктор физ.-мат. наук, профессор Романовский Иосиф Владимирович

кандидат технических наук Нарвский Андрей Сергеевич

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

Санкт-Петербургский государственный

электротехнический университет «ЛЭТИ»

Защита диссертации состоится 24 декабря 2009 года в 15гй на заседании диссертационного совета Д212.227.06 при Санкт-Петербургском государственном университете информационных технологий, механики и оптики, 197101, Санкт-Петербург, ул . Кронверкский 49.

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

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

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

доктор технических наук, доцент

Л.С. Лисицына

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

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

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

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

• механизм эффективной формализации требований к автоматным программам;

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

• синхронизация требований и реализации автоматных программ (односторонняя).

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

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

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

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

в метода интеграции спецификации и реализации автоматных объектно-ориентированных программ;

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

• каталога рефакторингов.

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

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

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

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

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

• каталог рефакторингов автоматных программ, и доказательство эквивалентности программ до и после рефакторинга.

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

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

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

• в компании ООО «ИнтеллиДжей Лабе» при разработке системы учеты дефектов YouTrack.

• в учебный процесс по курсу «Применение автоматов в программировании» кафедры «Компьютерные технологии» Санкт-Петербургского государственного университета информационных технологий, механики и оптики (СПбГУ ИТМО).

Апробация диссертации. Основные положения диссертационной работы докладывались на III Межвузовской конференции молодых ученых (СПб., 2006 г.), XXXVI научной и учебно-методической конференции профессорско-преподавательского и научного состава СПбГУ ИТМО (2007 г.), конференциях Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE) (СПбГУ, 2008 г.), 5th Central and Eastern European Software Engineering Conference in Russia (SECR) (M., 2009 г.).

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

Гранты. Диссертация выполнялась в ходе работы над грантом для студентов, аспирантов вузов и академических институтов, находящихся на территории Санкт-Петербурга, который проводился Администрацией Санкт-Петербурга (2008 г.). Материалы диссертации используются в научно-исследовательской работе по теме «Методы повышения качества при разработке автоматных программ с использованием функциональных и объектно-ориентированных языков программирования», которая победила в конкурсе НК-421П «Проведение поисковых научно-исследовательских работ

по направлению «Информатика-», проводившемся в 2009 году Федеральным агентством по образованию по Федеральной целевой программе «Научные и научно-педагогические кадры инновационной России» на 2009-2013 годы.

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

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

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

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

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

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

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

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

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

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

Метод верификации на модели использует в качестве языка спецификаций один из языков темпоральной логики. Недостатком этих языков является сложность выражения требований к автоматным программам. Например, требование «Во время движения двери лифта закрыты» для автомата управления лифтом, рассматриваемого во второй главе, на языке линейной темпоральной логики (LTL) выражается следующей весьма сложной темпоральной формулой: [(Zj. V z2) => zT4J(z3 Vz^)] Л [z+ => (zj V z2)U (zs V (zt V z2))].

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

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

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

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

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

Таблица. Совместимость элементов автоматного интерфейса и видов контрактов

Предусловия Постусловия Инварианты

Состояния + ' + +

Группы состояний + + +

Входные воздействия + + -

Выходные воздействия + - -

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

Проверка выполнения контрактов, как и в объектно-ориентированном программировании, может выполняться как статически, так и динамически. При этом автором предлагается преобразовывать контракты в формулы линейной темпоральной логики, что может бьпъ выполнено автоматически. При статической проверке контракты используются в качестве спецификации для верификации методом Model Checking. Динамическая проверка контрактов основана на предложенном автором методе динамической верификации, описанном ниже. Этот метод в качестве спецификации использует формулы линейной темпоральной логики.

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

Известно, что любая £2Х-формула может бьпъ преобразована в альтернирующий автомат, прячем число состояний этого автомата линейно зависит от размера формулы. Таким образом, для верификации соответствия протокола работы программы и LTL-специфшсации, достаточно по этой спецификации построить альтернирующий автомат и проверить, принимается ли данный протокол полученным автоматом. Существуют три алгоритма, позволяющих выполнить такую проверку. В работе показана применимость этих алгоритмов к верификации автоматных программ и описан метод построения протоколов.

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

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

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

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

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

Таким образом, предлагается метод безопасного внесения изменений в автоматную программу, который состоит в разделении любого сложного изменения автомата на два этапа:

1. Рефакторинг автомата.

2. Набор модификаций, приводящих к изменению поведения автомата.

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

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

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

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

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

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

Рассматривается пример использования метода: модификация автомата управления банкоматом в связи с изменением числа попыток ввода /W-кода.

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

Текстовые языки в основном представлены автоматными расширениями статически типизированных языков программирования (таких как С# и Java), реализованных с помощью препроцессоров - инструментов, преобразующих код на языке программирования с автоматным расширением в код на языке программирования без такого расширения. Недостатком такого подхода является сложность расширения синтаксиса языка и сложность композиции расширений.

Рассматриваются два альтернативных подхода к решению проблемы интеграции автоматного и объектно-ориентированного кода. Первый из них основан на использовании возможностей динамических языков программирования. Рассматривается разработанная автором библиотека STROBE, реализующая автоматное расширение динамического языка программирования Ruby. Эта библиотека позволяет описывать поведение классов в терминах автоматов и реализует концепцию «автоматизированные объекты управления как классы». Методы библиотеки организованы таким образом, что ее программный интерфейс выглядит как набор конструкций предметно-ориентированного языка. При этом для клиентов автоматного класса он является обычным классом системы.

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

Поэтому для интеграции спецификации и кода автоматной программы целесообразно использовать метод, основанный на использовании мультиязыковых сред. В частности, в России компанией ООО «ИнтеллиДжей Лабе» разработана мультиязыковая среда JetBrains MPS. В этой среде программа представляется в виде абстрактного синтаксического дерева. При таком представлении программы различные расширения языков предоставляют наборы дополнительных возможных узлов абстрактного синтаксического дерева, и выбор между ними происходит явно, а не посредством неоднозначной трансляции. Узлы абстрактного синтаксического дерева являются концептами различных языков программирования. Редактирование этого дерева осуществляется с помощью редактора, который обеспечивает сходство процесса редактирования дерева с традиционным процессом редактирования текста программы. Это позволяет решить проблему комбинирования нескольких языков программирования. Использование комбинации предметно-ориентированных языков дает возможность описывать поведение программы в терминах предметной области. Для этой среды существует язык текстового автоматного программирования stateMachine, однако в нем не решена проблема интеграции кода автоматной программы и ее спецификации.

Для решения этой проблемы автором было разработано расширение языка stateMachine, названное stateSpec. Это расширение позволяет задавать спецификацию программы в виде формул линейной темпоральной логики и контрактов. При этом

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

Initial »tAto(ReadyToUsi) (

on unplugged do {<no statements?) transit to (TumedDft)

invariant (

voltajeTreahoid

currentVoltage < voltageTreshold

1

require lor RiadsTcUst isTurnedOn

}

1

specification {

G F ! (Broken) I P.eaclyToUse R TurnedOft cutrentVoltajt < voltageTreshold U Broken

)

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

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

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

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

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

Метод интеграции кода и спецификации автоматной программы, а также предметно-ориентированный язык stateSpec, описанные в данной работе, использовались:

• в компании ООО «ИнтеллиДжей Лабе» при разработке системы учета дефектов YouTrack,

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

Опишем внедрение более подробно. В компании ООО «ИнтеллиДжей Лабе», работающей на мировом рынке под торговой маркой JetBrains, разработана система учета дефектов YouTrack. Эта система реализована на базе среды мультиязыкового программирования MPS. Система представляет собой клиент-серверное интернет-приложение, в котором клиентская часть выполняется в интернет-обозревателе пользователя. Для уменьшения времени отклика в системе используется технология AJAX (Asynchronous Javascript And Xml).

Часть поведения системы, связанная с реализацией реактивных компонентов пользовательского интерфейса, реализована в виде автоматов на диалекте языка stateMachine, в котором в качестве базового используется язык JavaScript вместо языка Java. Эти автоматы получают на вход информацию о действиях пользователя и ответы, полученные от сервера. В качестве выходных воздействий используются команды обновления пользовательского интерфейса и выполнения запросов к серверу. Примерами автоматов являются автомат управления списком дефектов на экране и автомат управления интерфейсом строки поиска.

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

Заключение

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

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

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

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

4. Составлен каталог рефакторингов автоматных программ; представлено доказательство эквивалентности программы до и после рефакторинга.

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

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

1. Степанов О. Г., Шалыто А. А., Шопырин Д. Г. Предметно-ориентированный язык автоматного программирования на базе динамического языка RUBY // Информационно-управляющие системы. 2007. № 4, с.22-27.

2. Степанов О. Г. Метод автоматической динамической верификации автоматных программ // Научно-технический вестник СПбГУ ИТМО. № 53, с.221-229.

3. Stepanov О., Shalyto A. A Method for Automatic Runtime Verification of Automata-Based Programs // Proceedings of Spring/Summer Young Researchers' Colloquium on Software Engineering 2008, Vol. 2, pp. 19-23.

4. Борисенко А., Федотов П., Степанов О., Шалыто А. Разработка надежного программного обеспечения со сложным поведением // Сборник трудов конференции 5th Central and Eastern European Software Engineering Conference in Russia c. 125-128.

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

ОГЛАВЛЕНИЕ.

ВВЕДЕНИЕ.

ГЛАВА 1. МЕТОДЫ РЕАЛИЗАЦИИ ОБЪЕКТНО

ОРИЕНТИРОВАННЫХ И АВТОМАТНЫХ ПРОГРАММ.

1.1. Структура объектно-ориентированных программ.

1.2. Методы повышения качества объектно-ориентированных программ.

1.3. Автоматное объектно-ориентированное программирование

1.4. Методы повышения качества автоматных объектно-ориентированных программ.

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

ГЛАВА 2. ФОРМАЛИЗАЦИЯ ТРЕБОВАНИЙ К АВТОМАТНЫМ ОБЪЕКТНО-ОРИЕНТИРОВАННЫМ ПРОГРАММАМ.

2.1. Формализация требований к автоматным программам.

2.2. Интерфейсы автоматных объектов.

2.3. Автоматное программирование по контрактам.

2.4. Способы проверки автоматных контрактов.

2.5. Динамический метод проверки спецификаций автоматных программ.

2.6. Формализация требований к автоматным программам.

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

ГЛАВА 3. ВНЕСЕНИЕ ИЗМЕНЕНИЙ В АВТОМАТНЫЕ ПРОГРАММЫ.

3.1. Внесение изменений в автоматные программы.

3.2. Классификация изменений автоматных программ.

3.3. Описание базовых изменений автоматов.

3.3.1. Добавление состояния.

3.3.2. Удаление состояния.

3.3.3. Установка начального состояния.

3.3.4. Снятие начального состояния.

3.3.5. Добавление конечного состояния.

3.3.6. Удаление конечного состояния.

3.3.7. Добавление перехода.

3.3.8. Изменение события на переходе.

3.3.9. Изменение условия на переходе.

3.3.10. Удаление перехода.

3.3.11. Перемещение перехода.

3.4. Рефакторинг автоматных программ.

3.4.1. Группировка состояний.

3.4.2. Удаление группы состояний.

3.4.3. Слияние состояний.

3.4.4. Выделение автомата.

3.4.5. Встраивание вызываемого автомата.

3.4.6. Переименование состояния.

3.4.7. Перемещение воздействия из состояния в переходы.

3.4.8. Перемещение воздействия из переходов в состояние.

3.5. Метод внесения изменений в автоматные программы.

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

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

ГЛАВА 4. ИНТЕГРАЦИЯ СПЕЦИФИКАЦИИ И КОДА АВТОМАТНЫХ ОБЪЕКТНО-ОРИЕНТИРОВАННЫХ ПРОГРАММ.

4.1. Автоматное программирование в динамических языках.

4.1.1. Определение общих свойств автомата.

4.1.2. Описание графов переходов.

4.1.3. Пример декларации автомата.

4.1.4. Использование библиотеки.

4.1.5. Реализация библиотеки.

4.1.6. Отладка программ.

4.1.7. Взаимодействие с окружением.

4.1.8. Формализация спецификаций автоматов.

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

4.2.1. Описание языков в системе JetBrains MPS.

4.2.2. Автоматное программирование в среде JetBrains MPS.

4.2.3. Язык спецификации автоматов.

4.2.4. Реализация языка спецификации автоматов.

4.2.5. Пример использования языка спецификации автоматов

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

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

5.1. Область внедрения.

5.2. Использование системы JetBrains MPS в программе YouTrack.

5.3. Автомат управления списком дефектов IssueList.js.

5.4. Автомат управления выпадающей подсказкой Suggest.js.

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

ЗАКЛЮЧЕНШ.

ИСТОЧНИКИ.

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

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

Эти недостатки сказываются на качестве модулей программ со ' сложным поведением, для которых тестирование оказывается наименее t эффективным. В модулях со сложным поведением реакция на вызов зависит от внутреннего состояния модуля. При этом в России с 1991 года разрабатывается концепция автоматного программирования, которая позволяет эффективно разрабатывать модули со сложным поведением [1]. Частью этой концепции являются технологии совмещения автоматного и объектно-ориентированного программирования. Это позволяет реализовывать модули со сложным поведением с использованием автоматного программирования в различных проектах, включая уже существующие.

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

- механизм эффективной формализации требований к автоматным программам;

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

- синхронизация требований и реализации автоматных программ (односторонняя).

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

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

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

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

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

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

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

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

- каталог рефакторингов автоматных программ, и доказательство эквивалентности программ до и после рефакторинга.

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

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

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

- в компании ООО «ИнтеллиДжей Лабе» при разработке системы учеты дефектов YouTrack.

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

Апробация диссертации. Основные положения диссертационной работы докладывались на III Межвузовской конференции молодых ученых (СПб., 2006 г.), XXXVI научной и учебно-методической конференции профессорско-преподавательского и научного состава СПбГУ ИТМО (2007 г.), конференциях Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE) (СПбГУ, 2008 г.), 5th Central and Eastern European Software Engineering Conference in Russia (SECR) (M., 2009 г.).

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

Гранты. Диссертация выполнялась в ходе работы над грантом для студентов, аспирантов вузов и академических институтов, находящихся на территории Санкт-Петербурга, который проводился Администрацией Санкт-Петербурга (2008 г.). Материалы диссертации используются в научно-исследовательской работе по теме «Методы повышения качества при разработке автоматных программ с использованием функциональных и объектно-ориентированных языков программирования», которая победила в конкурсе НК-421П «Проведение научных исследований научными группами под руководством кандидатов наук» по направлению «Информатика», который был объявлен в 2009 году Федеральным агентством по образованию по Федеральной целевой программе «Научные и научно-педагогические кадры инновационной России» на 2009-2013 годы.

Структура диссертации. Диссертация изложена на 150 страницах и состоит из введения, пяти глав и заключения. Список литературы содержит 69 наименований. Работа содержит 24 рисунка и одну таблицу. В первой главе приведен обзор современных методов реализации объектно-ориентированных и автоматных программ. Во второй главе предложен метод формализации требований к автоматным программам на основе использования контрактов, темпоральных спецификаций, а также статической и динамической верификации. В третьей главе предлагаются метод рефакторинга автоматных программ и метод их модификации, уменьшающий число изменений, которые могут привести к появлению ошибок. В четвертой главе предложен метод интеграции спецификации и кода автоматных программ на основе использования возможностей мультиязыковых сред. В пятой главе излагаются результаты внедрения

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

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

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

ЗАКЛЮЧЕНИЕ

В настоящей работе разработаны методы реализации автоматных объектно-ориентированных программ. Эти методы позволяют:

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

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

- интегрировать код и спецификацию автоматных объектно-ориентированных программ;

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

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

Созданный язык был использован для формализации спецификаций компонентов интерфейса программы YouTrack. Благодаря использованию языка stateSpec удалось представить требования к этим компонентам в виде контрактов и темпоральных спецификаций и провести верификацию.

Основными направлениями развития полученных результатов автор считает следующие:

- автоматизация рефакторингов автоматных программ;

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

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

1. Шалыто А. А. Switch-технология. Алгоритмизация и программирование задач логического управления. СПб.: Наука, 1998. http://is.ifmo.ru/books/switch/l

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

3. Мейер Б. Объектно-ориентированное конструирование программных систем. М.: Интернет-университет информационных технологий, 2005.

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

5. Kurzweil R. The Singularity Is Near: When Humans Transcend Technology. Penguin, 2006.

6. Beck K., Andres C. Extreme Programming Explained: Embrace Change (2nd Edition). Addison-Wesley Professional, 2004.

7. Schwaber K. Agile Project Management with Scrum. Microsoft Press, 2004.

8. Turner M. Microsoft Solutions Framework Essentials. Microsoft Press, 2006.

9. Alexander C. A Pattern Language: Towns, Buildings, Construction. USA: Oxford University Press, 1977.

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

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

12. Канер С., Фолк Д., Нгуен Е. Тестирование программного обеспечения. Киев: ДиаСофт, 2000.

13. Ахо А., Лам М., Сети Р., Ульман Д. Компиляторы. Принципы, технологии и инструментарий. Вильяме, 2008.

14. Lyu M.R., Horgan J.R., London S. A coverage analysis tool for the effectiveness of software testing //IEEE Transactions on Reliability. 1994, № 43(4).

15. Веб-сайт каркаса JVnit. http://junit.org/

16. Веб-сайт каркаса NUnit. http://www.nunit.com/

17. Веб-сайт каркаса PyUnit. http://pyunit.sourceforge.net/

18. Дюваль П., Матиас С., Гловер Э. Непрерывная интеграция. Улучшение качества программного обеспечения и снижение риска. М.: Вильяме, 2008.

19. Мейер Б. Объектно-ориентированное конструирование программных систем. М.: Русская Редакция, 2005.

20. Wing J.M. Writing Larch interface language specifications //ACM Trans. Program. Lang. Syst. 1987, № 9.

21. Веб-сайт проекта Code Contracts компании Microsoft. http://research.microsoft.com/en-us/projects/contracts/

22. Веб-сайт проекта Contract4j. http://www.contract4i.org/contract4i

23. Bamett M., DeLine R., Fahndrich M., Leino K.Rustan M., Schulte W. Verification of object-oriented programs with invariants //Journal of Object Technology. 2004, № 6.

24. Шалыто А. А., Туккель H. И. Программирование с явным выделением состояний //Мир ПК. 2001, № 8, 9. http://is.ifmo.ru/works/mirk/

25. Шопырин Д. Г., Шалыто А. А. Объектно-ориентированный подход к автоматному программированию //Информационно-управляющие системы. 2003, № 5. http://is.ifmo.ru/works/ooaut/

26. Поликарпова Н. И., Шалыто А. А. Автоматное программирование. СПб.: Питер, 2010.

27. Гуров В. С. Технология проектирования и разработки объектно-ориентированных программ с явным выделением состояний (метод, инструментальное средство, верификация). Диссертация на соискание ученой степени кандидата технических наук. СПбГУ ИТМО, 2008.

28. Степанов О. Г. Предметно-ориентированный язык автоматного программирования на базе динамического языка Ruby. Магистерская диссертация. СПбГУ ИТМО, 2006.

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

30. Наумов Л. А. Объектно-ориентированное программирование с явным выделением состояний //Информационно-управляющие системы. 2003, № 6.

31. Фельдман П. И. Разработка средств для отладки автоматных программ, построенных на основе предложенной библиотеки классов. СПбГУ ИТМО, 2004. http://is.ifmo.ru/papers/aut dlf/

32. Астафуров А. А., Шалыто А. А. Декларативный подход к вложению и наследованию автоматных классов при использовании императивных языков программирования. Software Engineering Conference (Russia). M.: TEKAMA, 2007.

33. Гуров В. С., Мазин М. А., Шалыто А. А. Текстовый язык автоматного программирования // Научно-технический вестник СПбГУ ИТМО. 2008, № 53. http://is.ifmo.ru/works/2007 10 05 mps textual language.pdf

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

35. Дмитриев С. Языково-ориентированное программирование: следующая парадигма. 2005. http://www.rsdn.ru/article/philosophy/LOP.xml

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

37. Степанов О. Г., Шалыто А. А., Шопырин Д. Г. Предметно-ориентированный язык автоматного программирования на базе динамического языка Ruby. 2007. http://is.ifmo.ru/works/ 2007 10 05 aut lang.pdf

38. Астафуров А., Тимофеев К, Шалыто А. Наследование автоматных классов с использованием динамических языков программирования на примере Ruby. М.: ТЕКАМА, 2008. http://www.secr.ru/?pageid=4548&submissionid=5270

39. Бурдонов И. Б., Косачев А. С., Кулямин В. В. Использование конечных автоматов для тестирования программ //Программирование. 2000, № 26.

40. Гуров В. С., Мазин М. А., Шалыто А. А. Ядро автоматного программирования. Свидетельство о государственной регистрации программы для ЭВМ. 2006.

41. Грис Д. Наука программирования. М.: Мир, 1984.

42. Непомнящий В. А., Рякин О. М. Прикладные методы верификации программ. М.: Радио и связь, 1988.

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

44. Pnueli A. The Temporal Logic of Programs / Proceedings of the 18-th IEEE Symposium on Foundation of Computer Science. 1977.

45. Кузьмин E. В., Соколов В. А. Моделирование, спецификация и верификация «автоматных» программ //Программирование. 2008, № 1.

46. Вельдер С. Э., Шалыто А. А. О верификации простых автоматных программ на основе метода Model Checking //Информационно-управляющие системы. 2007, № 3.

47. Яминов Б. Р., Шалыто А. А. Расширение верификатора Bagor для верификации автоматных UniMod-моделей. Свидетельство о государственной регистрации программы для ЭВМ. 2008.

48. Лукин М. А., Шалыто А. А. Трансляция UniMod-модели во входной язык верификатора SPIN. Свидетельство о государственной регистрации программы для ЭВМ. 2008.

49. Kurbatsky Е. Verification of Automata-Based Programs. SPbSU, 2008.

50. Emerson E.A. Temporal and modal logic. MIT Press, 1990.

51. Kalaji A., Hierons R.M., Swift S. Automatic Generation of Test Sequences form EFSM Models Using Evolutionary Algorithms. 2008.

52. Finkbeiner В., Sipma H. Checking Finite Traces Using Alternating Automata //Form. Methods Syst. Des. 2004, № 24.

53. Vardi M. Alternating Automata and Program Verification //Computer Science Today. Recent Trends and Developments. LNCS 1000. 1995.

54. M.Y. Vardi. Alternating Automata: Checking Truth and Validity for Temporal Logics. Springer-Verlag, 1997.

55. Havelund K., Ro§u G. Testing Linear Temporal Logic Formulae on Finite Execution Traces. 2001.

56. ФаулерМ. Рефакторинг. М.: Вильяме, 2003.

57. Кафедра «Технологии программирования». Раздел «Проекты». http://is.ifmo.ru/proiects/

58. Козлов В. А., Комалева В. А. Моделирование работы банкомата. СПбГУ ИТМО, 2006. http://is.ifmo.ru/unimod-proiects/bankomat/

59. Балтийский И. А., Гиндин С. И. Моделирование работы банкомата. СПбГУ ИТМО, 2008. http://is.ifmo.ru/unimod-proiects/atm/

60. Boo language website, http://boo.codehaus.org/

61. Nemerle language website, http://nemerle.org

62. Гуров В. С., Мазин М. А., Шалыто А. А. Операционная семантика UML-диаграмм состояний в программном пакете Unimod / Телематика-2005. СПбГУ ИТМО, 2005.

63. Cardelli L., Wegner P. On Understanding Types, Data Abstraction, and Polymorphism//Computing Surveys. 1985, №12.

64. 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.

65. Конопко К. С. HELGINS: универсальный язык для написания анализаторов типов // Компьютерные инструменты в образовании. 2007, № 4.68. MPS User's Guide.http://www.ietbrains.net/confluence/displav/MPS/MPS+User%27s+Guide

66. Гуров В. С., Мазин М. А., Шалыто А. А. Текстовый язык автоматного программирования //Научно-технический вестник СПбГУ ИТМО. 2007, №42.