ntvНаучно-технический вестник информационных технологий, механики и оптикиScientific and Technical Journal of Information Technologies, Mechanics and Optics2226-14942500-0373Университет ИТМО10.17586/2226-1494-2023-23-2-436-438ntv-390Research ArticleПИСЬМА В РЕДАКЦИЮВалидация автоматных спецификацийValidation of state machine specificationshttps://orcid.org/0000-0002-2723-2077ШалытоА. А.ShalytoA. A.

Шалыто Анатолий Абрамович — доктор технических наук, профессор, главный научный сотрудник, профессор, Санкт-Петербург, 197101

sc 56131789500

Anatoly A. Shalyto — D.Sc., Full Professor, Chief ResearcherSaint Petersburg, 197101sc 56131789500

shalyto@mail.ifmo.ruУниверситет ИТМОРоссияITMO UniversityRussian Federation202321122024232436438Copyright © Шалыто А.А., 20242024Шалыто А.А.Shalyto A.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://ntv.elpub.ru/jour/article/view/390

Изложен новый взгляд на обеспечение качества автоматных программ. При этом вместо термина «верификация автоматных программ» предложено использовать термины «верификация автоматных моделей» и «валидация автоматных спецификаций». Первый термин применим при наличии формальной спецификации, а второй — при ее отсутствии, что более характерно для практики. Это позволяет более осмысленно подходить к пониманию того, как обеспечивать качество автоматных программ .

The paper presents a new view on the quality assurance of state machine programs. Instead of the term “verification of state machine programs”, it is proposed to use the terms “verification of state machine models” and “validation of state machine specifications”. The first of which is applicable in the presence of a formal specification, and the second — in its absence, which is more typical for practice. This allows a more meaningful approach to understanding how to ensure the quality of state machine programs.

автоматыпрограммыспецификацияверификациявалидацияstate machineprogramsspecificationverificationvalidationReferencesКарпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем. СПб.: БХВ-Петербург, 2010. 560 с.Ka rpov Iu.G. Model Checking. Verification of Parallel and Distributed Software Systems. St. Petersburg, BHV Petersburg Publ., 2010, 560 p. (in Russian)Янкин Ю.Ю., Шалыто А.А. Автоматное программирование ПЛИС в задачах управления электроприводом // Информационно-управляющие системы. 2011. № 1. С. 50–56.Yankin Y.Y., Shalyto A.A. A method of finite-state machine realization in electric motor drives control. Information and Control Systems, 2011, no. 1, pp. 50–56. (in Russian)Вельдер С.Э., Лукин М.А., Шалыто А.А., Яминов Б.Р. Верификация автоматных программ. СПб.: Наука, 2011. 244 с.Velder S.E., Lukin M.A., Shalyto A.A., Iaminov B.R. Verification of Automata-Based Programs. St. Petersburg, Nauka Publ., 2011, 244 p. (in Russian)Кузьмин Е.В., Соколов В.А. Моделирование, спецификация и верификация «автоматных» программ // Программирование. 2008. Т. 34. № 1. С. 38–60.Kuzmin E.V., Sokolov V.A. Modeling, specification, and verification of automaton programs. Programming and Computer Software, 2008, vol. 34, no. 1, pp. 27–43. https://doi.org/10.1134/s0361768808010040Шалыто А.А. Логическое управление. Методы аппаратной и программной реализации алгоритмов. СПб.: Наука, 2000. 780 с.Shalyto A.A. Logical Control: Methods for Hardware and Software Implementation of Algorithms. St. Petersburg, Nauka Publ., 2000, 789 p. (in Russian)

The authors declare that there are no conflicts of interest present.