УДК 004.05

ВЕРИФИКАЦИЯ ПАРАЛЛЕЛЬНЫХ АВТОМАТНЫХ ПРОГРАММ

Лукин М.А.


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

Аннотация

Рассмотрен интерактивный метод верификации параллельных автоматных программ, в которых иерархические автоматы могут реализовываться в разных потоках и взаимодействовать друг с другом. Верификация проводится при помощи инструментального средства Spin, включает в себя автоматическое построение модели на языке Promela, приведение LTL-формулы в формат, определяемый инструментальным средством Spin и построение контрпримера в терминах автоматов. Интерактивная верификация позволяет сократить время верификации и увеличить максимально возможный размер верифицируемых программ. Рассмотренный метод позволяет верифицировать параллельную систему иерархических автоматов, которые взаимодействуют между собой через сообщения и общие переменные. Особенность автоматной модели состоит в том, что каждый автомат объявляется как новый тип данных и может иметь произвольное (но заранее заданное) число экземпляров. Каждый конечный автомат в системе может запускать другой автомат в новом потоке или иметь вложенный автомат. Была проведена апробация инструментального средства Stater, разработанного на основе данного метода. На всех примерах Stater отработал правильно.


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

Список литературы
1. Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ:  Model Checking М.: МЦНМО, 2002. 416 с.
2. Вельдер С.Э., Лукин М.А., Шалыто А.А., Яминов Б.Р. Верификация автоматных программ. СПб: Наука, 2011. 244 с.
3. Карпов Ю.Г. Model Checking: верификация параллельных и распределенных программных систем. СПб: БХВ-Петербург, 2010. 560
4. Официальный сайт инструментального средства http://spinroot.com, свободный. Яз. англ. (дата обращения 03.09.2013).
5. Gnesi S., Mazzanti F. On the fly model checking of communicating UML state machines. 2004 [Электрон- ный ресурс]. Режим доступа: http://fmt.isti.cnr.it/WEBPAPER/onthefly-SERA04.pdf, свободный. Яз. англ. (дата обращения 25.11.2013).
6. Gnesi S., Mazzanti F. A model checking verification environment for UML statecharts // Proc. of XLIII Congresso Annuale AICA. 2005 [Электронный ресурс]. Режим доступа: http://fmt.isti.cnr.it/~gnesi/matdid/aica.pdf, свободный. Яз. англ. (дата обращения 20.07.2013).
7. Канжелев С.Ю., Шалыто А.А. Автоматическая генерация автоматного кода // Информационно- управляющие системы. 2006. № 6 (25). С. 35–42.
8. Виноградов Р.А., Кузьмин Е.В., Соколов В.А. Верификация автоматных программ средствами CPN/Tools // Моделирование и анализ информационных систем. 2006. Т. 13. № 2. С. 4–15.
9. Васильева К.А., Кузьмин Е.В. Верификация автоматных программ с использованием LTL // Модели- рование и анализ информационных систем. 2007. Т.14. № 1. С. 3–14.
10. Лукин М.А. Верификация автоматных программ. Бакалаврская работа. СПбГУ ИТМО, 2007 [Элек- тронный ресурс]. Режим доступа: http://is.ifmo.ru/papers/_lukin_bachelor.pdf, свободный. Яз. рус. (дата обращения 25.11.2013).
11. Яминов Б.Р. Автоматизация верификации автоматных UniMod-моделей на основе инструментального средства Bogor. Бакалаврская работа. СПбГУ ИТМО, 2007 [Электронный ресурс]. Режим доступа: http://is.ifmo.ru/papers/jaminov_bachelor.pdf, свободный. Яз. рус. (дата обращения 25.11.2013).
12. Вельдер С.Э., Шалыто А.А. О верификации простых автоматных систем на основе метода Model Checking // Информационно-управляющие системы. 2007. № 3 (28). С. 27–38.
13. Ma G. Model checking support for CoreASM: model checking distributed abstract state machines using Spin. 2007 [Электронный ресурс]. Режим доступа: http://summit.sfu.ca/item/8056, свободный. Яз. англ. (дата обращения 25.11.2013).
14. David A., Möller O., Yi W. Formal Verification of UML Statecharts with Real-time Extensions // Lecture Notes in Computer Science. 2002. V.2306. P. 218–232.
15. Егоров К.В., Шалыто А.А. Методика верификации автоматных программ // Информационно- управляющие системы. 2008. № 5 (36). С. 15–21.
16. Курбацкий Е.А. Верификация программ, построенных на основе автоматного подхода с использова- нием программного средства SMV // Научно-технический вестник СПбГУ ИТМО. 2008. № 8 (53). С. 137–144.
17. Лукин М.А., Шалыто А.А. Верификация автоматных программ с использованием верификатора SPIN // Научно-технический вестник СПбГУ ИТМО. 2008. № 8 (53). С. 145–162.
18. Гуров В.С., Яминов Б.Р. Верификация автоматных программ при помощи верификатора UNIMOD.VERIFIER // Научно-технический вестник СПбГУ ИТМО. 2008. № 8 (53). С. 162–176.
19. Егоров К.В., Шалыто А.А. Разработка верификатора автоматных программ // Научно-технический вестник СПбГУ ИТМО. 2008. № 8 (53). С. 177–188.
20. Гуров В.С., Мазин М.А., Шалыто А.А. Автоматическое завершение ввода условий в диаграммах со- стояний // Информационно-управляющие системы. 2008. № 1 (32). С. 24–33.
21. Prashanth C.M., Shet K.C. Efficient Algorithms for Verification of UML Statechart Models // Journal of Software. 2009. V. 4. N 3. P. 175–182.
22. Лукин М.А. Верификация визуальных автоматных программ с использованием инструментального средства SPIN. Магистерская диссертация. СПбГУ ИТМО, 2009 [Электронный ресурс]. Режим дос- тупа: http://is.ifmo.ru/papers/_lukin_master.pdf, свободный. Яз. рус. (дата обращения 25.11.2013).
23. Тимофеев К.И., Астафуров А.А., Шалыто А.А. Наследование автоматных классов с использованием динамических языков программирования (на примере языка RUBY) // Информационно-управляющие системы. 2009. № 4 (41). С. 21–25.
24. Ремизов А.О., Шалыто А.А. Верификация автоматных программ // Сборник докладов научно- технической конференции «Состояние, проблемы и перспективы создания корабельных информаци- онно-управляющих комплексов ОАО «Концерн Моринформсистема-Агат». М., 2010. С. 90–98 [Элек- тронный ресурс]. Режим доступа: http://is.ifmo.ru/works/_2010_05_25_verific.pdf, свободный. Яз. рус. (дата обращения 25.11.2013).
25. Клебанов А.А., Степанов О.Г., Шалыто А.А. Применение шаблонов требований к формальной спе- цификации и верификации автоматных программ // Семантика, спецификация и верификация про- грамм: теория и приложения: Труды семинара. 2010. С. 124–130 [Электронный ресурс]. Режим досту- па: http://is.ifmo.ru/works/_2010-10-01_klebanov.pdf, свободный. Яз. рус. (дата обращения 25.11.2013).
26. Вельдер С.Э., Шалыто А.А. Верификация автоматных моделей методом редуцированного графа пе- реходов // Научно-технический вестник СПбГУ ИТМО. 2009. № 6 (64). С. 66–77. 27. Янкин Ю.Ю., Шалыто А.А. Автоматное программирование ПЛИС в задачах управления электропри- водом // Информационно-управляющие системы. 2011. № 1 (50). С. 50–56


Creative Commons License

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License
Информация 2001-2024 ©
Научно-технический вестник информационных технологий, механики и оптики.
Все права защищены.

Яндекс.Метрика