МЕТОД РАЗРАБОТКИ WEB-ПРИЛОЖЕНИЙ НА ОСНОВЕ СИСТЕМ ИЕРАРХИЧЕСКИХ КОНЕЧНЫХ АВТОМАТОВ
КРАТКИЕ СООБЩЕНИЯ
УДК 658.512.011.56
А. А. ОЖИГАНОВ, А. И. ЧЕПУРНОЙ
МЕТОД РАЗРАБОТКИ WEB-ПРИЛОЖЕНИЙ НА ОСНОВЕ СИСТЕМ ИЕРАРХИЧЕСКИХ КОНЕЧНЫХ АВТОМАТОВ
Предлагается метод разработки web-приложений, позволяющий на основе задания формально верифицируемой модели иерархическими конечными автоматами обеспечить однозначное соответствие ей работающего приложения. Ключевые слова: web-приложение, конечный автомат, темпоральная логика, моделирование, программное обеспечение.
В настоящее время наблюдается значительный рост числа web-приложений с одновременным усложнением их функциональности. Поэтому существенную значимость приобретает повышение качества разработанных web-приложений.
В настоящей работе предлагается метод разработки web-приложений, основанный на использовании систем иерархических конечных автоматов. Метод состоит из следующих шагов.
1. Описывается обобщенная структура web-приложения [1]. 2. Осуществляется разбиение компонентов структуры на элементарные части, после чего описываются связи между ними [2]. 3. По полученному описанию задается формальная модель web-приложения в виде системы иерархических конечных автоматов. 4. Задается спецификация для приложения в целом и отдельных его компонентов (в терминах конечных автоматов или темпоральных логик CTL/LTL) [3]. 5. Осуществляется автоматическая проверка модели на соответствие спецификации. Если в процессе верификации обнаруживается несоответствие модели спецификации, выдается сообщение об ошибке. В данном случае необходимо вернуться к шагам 2—4 и исправить ошибку. Если ошибок не обнаружено, осуществляется переход к шагу 6. 6. На основе модели генерируется XML-описание переходов в приложении. 7. Разрабатывается исходный код элементов web-приложения, описанных в XML, например, на языках Java/JSP, PHP, Ruby и т.п. Предложенный метод позволяет значительно уменьшить число ошибок в web-приложениях за счет однозначного соответствия разработанного web-приложения формально верифицируемой модели.
СПИСОК ЛИТЕРАТУРЫ
1. Szyperski C. Component Software: Beyond Object-Oriented Programming. Addison-Wesley, 1999. 411 p. 2. Ожиганов А. А., Чепурной А. И. Классификация связей между частями web-приложения и его описание с
использованием модели конечных автоматов // Науч.-технич. вестн. СПбГУ ИТМО. 2009. Вып. 59. С. 100—106.
ИЗВ. ВУЗОВ. ПРИБОРОСТРОЕНИЕ. 2010. Т. 53, № 10
90 В. С. Ермолаев, М. В. Иночкин, И. П. Пузык, Л. В. Хлопонин, М. В. Пузык
3. Кларк Э. М. мл., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. М.: МЦНМО, 2002. 416 с.
Сведения об авторах Александр Аркадьевич Ожиганов — д-р техн. наук, профессор; Санкт-Петербургский государственный
университет информационных технологий, механики и оптики, кафедра вычислительной техники; E-mail: ojiganov@mail.ifmo.ru Александр Иванович Чепурной — аспирант; Санкт-Петербургский государственный университет информационных технологий, механики и оптики, кафедра вычислительной техники; E-mail: alexch@bk.ru
Рекомендована кафедрой вычислительной техники
Поступила в редакцию 06.08.10 г.
ИЗВ. ВУЗОВ. ПРИБОРОСТРОЕНИЕ. 2010. Т. 53, № 10
УДК 658.512.011.56
А. А. ОЖИГАНОВ, А. И. ЧЕПУРНОЙ
МЕТОД РАЗРАБОТКИ WEB-ПРИЛОЖЕНИЙ НА ОСНОВЕ СИСТЕМ ИЕРАРХИЧЕСКИХ КОНЕЧНЫХ АВТОМАТОВ
Предлагается метод разработки web-приложений, позволяющий на основе задания формально верифицируемой модели иерархическими конечными автоматами обеспечить однозначное соответствие ей работающего приложения. Ключевые слова: web-приложение, конечный автомат, темпоральная логика, моделирование, программное обеспечение.
В настоящее время наблюдается значительный рост числа web-приложений с одновременным усложнением их функциональности. Поэтому существенную значимость приобретает повышение качества разработанных web-приложений.
В настоящей работе предлагается метод разработки web-приложений, основанный на использовании систем иерархических конечных автоматов. Метод состоит из следующих шагов.
1. Описывается обобщенная структура web-приложения [1]. 2. Осуществляется разбиение компонентов структуры на элементарные части, после чего описываются связи между ними [2]. 3. По полученному описанию задается формальная модель web-приложения в виде системы иерархических конечных автоматов. 4. Задается спецификация для приложения в целом и отдельных его компонентов (в терминах конечных автоматов или темпоральных логик CTL/LTL) [3]. 5. Осуществляется автоматическая проверка модели на соответствие спецификации. Если в процессе верификации обнаруживается несоответствие модели спецификации, выдается сообщение об ошибке. В данном случае необходимо вернуться к шагам 2—4 и исправить ошибку. Если ошибок не обнаружено, осуществляется переход к шагу 6. 6. На основе модели генерируется XML-описание переходов в приложении. 7. Разрабатывается исходный код элементов web-приложения, описанных в XML, например, на языках Java/JSP, PHP, Ruby и т.п. Предложенный метод позволяет значительно уменьшить число ошибок в web-приложениях за счет однозначного соответствия разработанного web-приложения формально верифицируемой модели.
СПИСОК ЛИТЕРАТУРЫ
1. Szyperski C. Component Software: Beyond Object-Oriented Programming. Addison-Wesley, 1999. 411 p. 2. Ожиганов А. А., Чепурной А. И. Классификация связей между частями web-приложения и его описание с
использованием модели конечных автоматов // Науч.-технич. вестн. СПбГУ ИТМО. 2009. Вып. 59. С. 100—106.
ИЗВ. ВУЗОВ. ПРИБОРОСТРОЕНИЕ. 2010. Т. 53, № 10
90 В. С. Ермолаев, М. В. Иночкин, И. П. Пузык, Л. В. Хлопонин, М. В. Пузык
3. Кларк Э. М. мл., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. М.: МЦНМО, 2002. 416 с.
Сведения об авторах Александр Аркадьевич Ожиганов — д-р техн. наук, профессор; Санкт-Петербургский государственный
университет информационных технологий, механики и оптики, кафедра вычислительной техники; E-mail: ojiganov@mail.ifmo.ru Александр Иванович Чепурной — аспирант; Санкт-Петербургский государственный университет информационных технологий, механики и оптики, кафедра вычислительной техники; E-mail: alexch@bk.ru
Рекомендована кафедрой вычислительной техники
Поступила в редакцию 06.08.10 г.
ИЗВ. ВУЗОВ. ПРИБОРОСТРОЕНИЕ. 2010. Т. 53, № 10