ПОСТРОЕНИЕ АВТОМАТНЫХ ПРОГРАММ ПО СПЕЦИФИКАЦИИ С ПОМОЩЬЮ МУРАВЬИНОГО АЛГОРИТМА НА ОСНОВЕ ГРАФА  
МУТАЦИЙ

Чивилихин Даниил Сергеевич, Ульянцев Владимир Игоревич, Вяткин Валерий Владимирович, Шалыто Анатолий Абрамович

2014 , ТОМ 14, НОМЕР 6 ( ноябрь-декабрь )

ISSN 2226-1494 (print), ISSN 2500-0373 (online)

Меню

Публикации

Главный редактор

НИКИФОРОВ
Владимир Олегович
д.т.н., профессор

Партнеры

УДК 004.4'242

ПОСТРОЕНИЕ АВТОМАТНЫХ ПРОГРАММ ПО СПЕЦИФИКАЦИИ С ПОМОЩЬЮ МУРАВЬИНОГО АЛГОРИТМА НА ОСНОВЕ ГРАФА МУТАЦИЙ

Чивилихин Д.С., Ульянцев В.И., Вяткин В.В., Шалыто А.А.

Читать статью полностью

Язык статьи - Русский

Аннотация

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

Ключевые слова: конечный автомат, муравьиный алгоритм, верификация

Благодарности. Работа выполнена при государственной финансовой поддержке ведущих университетов Российской Федерации (субсидия 074-U01), при поддержке РФФИ в рамках научного проекта № 14-07-31337 мол_а.

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

1. Clarke E.M., Grumberg O., Peled D.A. Model Checking. MIT press, 1999. 330 p.

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

3. Егоров К.В., Царев Ф.Н., Шалыто А.А. Применение генетического программирования для построения автоматов управления системами со сложным поведением на основе обучающих примеров и

спецификации // Научно-технический вестник СПбГУ ИТМО. 2010. № 5 (69). С. 81–86.

4. Tsarev F., Egorov K. Finite state machine induction using genetic algorithm based on testing and model checking // Proc. 13th Annual Genetic and Evolutionary Computation Conference, GECCO'11. Dublin, Ireland,

2011. P. 759–762.

5. Yang C.-H., Vyatkin V., Pang C. Model-driven development of control software for distributed automation: a survey and an approach // IEEE Transactions on Systems, Man, and Cybernetics: Systems. 2014. V. 44. N

3. P. 292–305.

6. Chivilikhin D., Ulyantsev V. MuACOsm – a new mutation-based ant colony optimization algorithm for learning finite-state machines // Proc. 15th Genetic and Evolutionary Computation Conference, GECCO 2013. Amsterdam, Netherlands, 2013. P. 511–518.

7. Чивилихин Д.С., Ульянцев В.И., Шалыто А.А. Муравьиный алгоритм для построения автоматных программ по спецификации // Труды XII Всероссийского совещания по проблемам управления ВСПУ-2014. Москва, 2014. С. 4531–4542.

8. Егоров К.В. Генерация управляющих конечных автоматов на основе генетического программирования и верификации: дис. … канд. техн. наук. СПб.: НИУ ИТМО, 2013. 150 с.

9. Вельдер С.Э., Лукин М.А., Шалыто А.А., Яминов Б.Р. Верификация автоматных программ. СПб: Наука, 2011. 244 с.

10. Ульянцев В.И. Построение управляющих конечных автоматов по сценариям работы на основе решения задачи удовлетворения ограничений: магистерская диссертация [Электронный ресурс]. Режим

доступа: http://is.ifmo.ru/diploma-theses/2013/master/ulyantsev/ulyantsev.pdf, свободный. Яз. рус. (дата обращения 30.09.2014).

11. Скобцов Ю.А., Федоров Е.Е. Метаэвристики. Донецк: НОУЛИДЖ, 2013. 426 с.

12. Dorigo M., Stützle T. Ant Colony Optimization. MIT Press, 2004. 319 p.

13. López-Ibáñez M., Dubois-Lacoste J., Stützle T., Birattari M. The irace package: iterated race for automatic algorithm configuration. Technical Report TR/IRIDIA/2011-004. IRIDIA, Belgium, 2011. 20 p.

14. Wilcoxon F. Probability tables for individual comparisons by ranking methods // Biometrics. 1947. V. 3. P. 119–122.

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License