10.14489/vkit.2022.10.pp.056-062

DOI: 10.14489/vkit.2022.10.pp.056-062

Юртаев А. Г., Степанов М. Ф., Петров Д. Ю., Федоров В. А.
ВЕРИФИКАЦИЯ АВТОМАТОВ МЕТОДОМ MODEL CHECKING
(с. 56-62)

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

Ключевые слова: автоматизация; верификация; темпоральная логика; model checking.

Yurtaev A. G., Stepanov M. F., Petrov D. Yu., Fedorov V. A.
VERIFICATION OF AUTOMATONS BY MODEL CHECKING METHOD
(pp. 56-62)

Abstract. The article analyzes software verification of control systems based on finite state machines, presents a classification of software correctness checks, advantages and disadvantages of various approaches to software verification, and, as a result, justifies the use of static verification methods, namely the model checking method. To solve applied problems, it is proposed to use the NuSMV software verifier. A brief overview of NuSMV verifier is given. The route of verification of software written in automaton style by the method of model checking is described. Each stage is described in the example of two interacting automata method. The construction of the model is described from a verbal description of its transformation into a finite state machine model with intermediate states and the transformation of the automaton into a formal finite state machine model in the SMV language, which is the input data for the NuSMV verifier. A description of the requirements for the model is presented, ranging from a verbal description of the requirements to the formalization of requirements in language of the temporal logic CTL. Based on the obtained model in SMV language and the obtained formalization of the requirements in CTL temporal logic language, NuSMV verifier checks the feasibility of the obtained requirements on the obtained model of the automata system. An analysis of the results of verification according to the specified requirements is given. For verification, an error was introduced into the model, leading to a negative result of the feasibility of the specified requirements. The verifier indicated the presence of an error and the path leading to it. Based on the results of the analysis of the results, a conclusion is made about the need to use this verification method in tasks of responsible applications. Further steps for the development and implementation of this method are described.

Keywords: Automation; Verification; Temporal logic; Model checking.

+ - Информация об авторах (About the Authors) Click to collapse

Рус

А. Г. Юртаев, М. Ф. Степанов, Д. Ю. Петров, В. А. Федоров (Саратовский государственный технический университет имени Гагарина Ю. А., Саратов, Россия) E-mail: Этот e-mail адрес защищен от спам-ботов, для его просмотра у Вас должен быть включен Javascript

Eng

A. G. Yurtaev, M. F. Stepanov, D. Yu. Petrov, V. A. Fedorov (Yuri Gagarin State Technical University of Saratov, Saratov, Russia) E-mail: Этот e-mail адрес защищен от спам-ботов, для его просмотра у Вас должен быть включен Javascript

+ - Библиографический список (References) Click to collapse

Рус

1. Поликарпова Н. И., Шалыто А. А. Автоматное программирование. СПб.: ИТМО, 2008. 167 с.
2. Юртаев А. Г., Степанов М. Ф., Петров Д. Ю. Анализ возможностей верификации программного обеспечения на основе автоматного программирования // Сб. трудов «Современные технологии и автоматизация в технике, управлении и образовании» IV Междунар. науч.-практ. конф.; под общей ред. В. М. Земскова. Балаково: НИЯУ МИФИ, 2022. Т. 1. С. 185–189.
3. Кларк Э. М., Грамберг мл. О., Пелед Д. Верификация моделей программ: Model checking. М: МЦНМО, 2002. 416 с.
4. NuSMV User Manual [Электронный ресурс]. URL: https:// https://nusmv.fbk.eu/NuSMV/userman/index-v2.html (дата обращения: 15.03.2022).
5. Вельдер С. Э., Лукин М. А., Шалыто А. А., Яминов Б. Р. Верификация автоматных программ. СПб.: Наука, 2011. 244 с.
6. McMillan K. L. Symbolic Model Checking. Kluwer Academic Publ., 1993.
7. NuSMV 2: An OpenSource Tool for Symbolic Model Checking / A. Cimatti, E. Clarke, E. Giunchiglia, et al. // 14th International Conference Computer Aided Verification (CAV). 2002. 27–31 July 2002. Copenhagen, Denmark. P. 359 – 364.
8. Cimatti A., Clarke E., Giunchiglia F., Roveri M. NUSMV: a New Symbolic Model Checker // International Journal on Software Tools for Technology Transfer. 2000. V. 2. P. 410 – 425.
9. Kim Y., Jung J., Matsona E. An Adaptive Task-Based Model for Autonomous Multi-Robot Using HARMS and NuSMV // Procedia Computer Science. 2015. No. 56. P. 127 – 132.
10. Logic Controllers Dependability Verification Using a Plant Model / J. Machado, B. Denis, J. Lesage, et al. // 3d IFAC Workshop on Discrete-Event Sistem Design (DESD-06). 26 – 28 September 2006. Rydzyna, Poland. V. 39, Is. 17. P. 37 – 42.
11. Карпов Ю. Г. Model Checking. Верификация параллельных и распределенных программных систем. СПб.: БХВ, 2010. 510 с.

Eng

1. Polikarpova N. I., Shalyto A. A. (2008). Automatic programming. Saint Petersburg: ITMO. [in Russian language]
2. Yurtaev A. G., Stepanov M. F., Petrov D. Yu. (Eds.) (2021). Analysis of software verification capabilities based on automatic programming. Modern technologies and automation in engineering, management and education: IV International Scientific and Practical Conference. Balakovo: BITI. [in Russian language]
3. Klark E. M., Gramberg ml. O., Peled D. (2002). Verification of program models: Model checking. Moscow: MTsNMO. [in Russian language]
4. NuSMV User Manual. Available at: https://nusmv.fbk.eu/NuSMV/userman/index-v2.html (Accessed: 15.03.2022).
5. Vel'der S. E., Lukin M. A., Shalyto A. A., Yaminov B. R. (2011). Verification of automatic programs. Saint Petersburg: Nauka. [in Russian language]
6. McMillan K. L. (1993). Symbolic Model Checking. Kluwer Academic Publishers.
7. Cimatti A., Clarke E., Giunchiglia E. et al. (2002). NuSMV 2: An OpenSource Tool for Symbolic Model Checking. CAV 2002: Computer Aided Verification, pp. 359 – 364.
8. Cimatti A., Clarke E., Giunchiglia F., Roveri M. (2000). NUSMV: a New Symbolic Model Checker. International Journal on Software Tools for Technology Transfer, Vol. 2, pp. 410 – 425.
9. Kim Y., Jung J., Matsona E. (2015). An Adaptive Task-Based Model for Autonomous Multi-Robot Using HARMS and NuSMV. Procedia Computer Science, 56, pp. 127 – 132.
10. Machado J., Denis B., Lesage J. et al. (2006). Logic Controllers Dependability Verification Using a Plant Model. 3rd IFAC Workshop on Discrete-Event Sistem Design (DESD-06), Vol. 39, 17, pp. 37 – 42. Rydzyna.
11. Karpov Yu. G. (2010). Model Checking. Verification of parallel and distributed software systems. Saint Petersburg: BHV. [in Russian language]

+ - Заказать электронную версию статьи (Purchase digital version of a single article) Click to collapse

Рус

Статью можно приобрести в электронном виде (PDF формат).

Стоимость статьи 500 руб. (в том числе НДС 20%). После оформления заказа, в течение нескольких дней, на указанный вами e-mail придут счет и квитанция для оплаты в банке.

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

Для заказа скопируйте doi статьи:

10.14489/vkit.2022.10.pp.056-062

и заполните форму

Отправляя форму вы даете согласие на обработку персональных данных.

Eng

This article is available in electronic format (PDF).

The cost of a single article is 500 rubles. (including VAT 20%). After you place an order within a few days, you will receive following documents to your specified e-mail: account on payment and receipt to pay in the bank.

After depositing your payment on our bank account we send you file of the article by e-mail.

To order articles please copy the article doi:

10.14489/vkit.2022.10.pp.056-062

and fill out the form