Меню
Публикации
2024
2023
2022
2021
2020
2019
2018
2017
2016
2015
2014
2013
2012
2011
2010
2009
2008
2007
2006
2005
2004
2003
2002
2001
Главный редактор
![](/pic/nikiforov.jpg)
НИКИФОРОВ
Владимир Олегович
д.т.н., профессор
Партнеры
УДК 004.4'242
Чивилихин Д.С., Ульянцев В.И., Вяткин В.В., Шалыто А.А.
Читать статью полностью
ПОСТРОЕНИЕ АВТОМАТНЫХ ПРОГРАММ ПО СПЕЦИФИКАЦИИ С ПОМОЩЬЮ МУРАВЬИНОГО АЛГОРИТМА НА ОСНОВЕ ГРАФА МУТАЦИЙ
Читать статью полностью
![](/images/pdf.png)
Язык статьи - Русский
Аннотация
Аннотация
Традиционный в области разработки программ процесс тестирования не может гарантировать их корректности, поэтому при повышенных требованиях к надежности программ прибегают к верификации. Верификация позволяет проверять некоторые свойства программы во всех возможных ее состояниях, однако сам процесс верификации сложен. В методе проверки моделей (model checking) строится модель программы (обычно вручную), а требования к ней записываются на языке темпоральной логики. Выполнение или невыполнение этих требований к модели может быть проверено автоматически. Основной проблемой такого подхода является разрыв между программой и ее моделью. Парадигма автоматного программирования позволяет устранить указанный разрыв. В автоматном программировании логика работы программ описывается управляющими конечными автоматами, модели которых могут быть построены автоматически. В работе рассматривается применение муравьиного алгоритма на основе графа мутаций для решения задач построения автоматных программ по их спецификации, заданной сценариями работы и темпоральными свойствами. Апробация предложенного подхода проведена на примере задачи построения автомата управления дверьми лифта, а также на случайных данных. Полученные результаты показывают, что муравьиный алгоритм в два–три раза эффективнее ранее применявшегося генетического. Предложенный подход может быть рекомендован для автоматизированного построения управляющих программ для ответственных систем.
Ключевые слова: конечный автомат, муравьиный алгоритм, верификация
Благодарности. Работа выполнена при государственной финансовой поддержке ведущих университетов Российской Федерации (субсидия 074-U01), при поддержке РФФИ в рамках научного проекта № 14-07-31337 мол_а.
Список литературы
Благодарности. Работа выполнена при государственной финансовой поддержке ведущих университетов Российской Федерации (субсидия 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.