informИнформатикаInformatics1816-03012617-6963UIIP NASBinform-584Research ArticleЛОГИЧЕСКОЕ ПРОЕКТИРОВАНИЕLOGICAL DESIGNВерификация систем с параллелизмом поведения на основе графа достижимых состоянийVerification of systems with behavior parallelism on the basis of the graph of reachable statesПоттосинЮ. В.PottosinYu. V.

Поттосин Юрий Васильевич, кандидат физикоматематических наук, ведущий научный сотрудник

Yuri V. Pottosin, Cand. Sci. (Phys.-Math.), Leading Researcher

pott@newman.bas-net.byРомановВ. И.RomanovV. I.

Романов Владимир Ильич, кандидат технических наук, ведущий научный сотрудник

Vladimir I. Romanov, Cand. Sci. (Eng.), Leading Researcher

rom@newman.bas-net.byЧеремисиноваЛ. Д.CheremisinovaL. D.

Черемисинова Людмила Дмитриевна, доктор технических наук, главный научный сотрудник

Ljudmila D. Cheremisinova, Dr. Sci. (Eng.), Chief Researcher

cld@newman.bas-net.byОбъединенный институт проблем информатики Национальной академии наук БеларусиThe United Institute of Informatics Problems of the National Academy of Sciences of BelarusОбъединенный институт проблем информатики Национальной академии наук БеларусиThe United Institute ofInformatics Problems of the National Academy of Sciences of Belarus2019061220181626272Copyright © Поттосин Ю.В., Романов В.И., Черемисинова Л.Д., 20192019Поттосин Ю.В., Романов В.И., Черемисинова Л.Д.Pottosin Y.V., Romanov V.I., Cheremisinova L.D.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://inf.grid.by/jour/article/view/584

Рассматривается задача верификации систем управления на основе моделей их поведения, которая состоит в проверке соответствия поведения системы требованиям, предъявляемым спецификацией на ее проектирование. Тестирование предполагает выполнение экспериментов, заключающихся в моделировании исследуемой системы, в ходе которого она проверяется на вход-выходное соответствие модели. Тестовая последовательность генерируется на основе модели, описывающей желаемое поведение системы. Предлагается метод построения тестовой последовательности для верификации схемной (или программной) реализации системы управления с параллелизмом поведения, который основан на обходе графа состояний, достижимых при функционировании системы. Описывается метод построения множества достижимых полных состояний для параллельного алгоритма описания поведения системы управления и получения тестовых наборов. Полагается, что описание функционирования системы, заданное спецификацией на проектирование, корректно; проверке подлежит схемная (или программная) реализация, которая должна соответствовать этой спецификации.

Considered problem of model based verification of control systems is the checking whether the system behavior satisfies the requirements fixed in the design specification The testing includes the experiments consisting in simulation of investigated system to see input-output correspondence to the model. The test sequence is generated on the basis of the model that describes the desired behavior of the system. The method to construct a test sequence for verification of hardware (or software) implementation of a control system with behavior parallelism is suggested that is based on traversal of the graph of the states that are reachable in system functioning. A method for constructing the set of reachable global states for a parallel algorithm of the control system behavior and a method to obtain the test sets are described. The description of the system functioning, which is given by the design specification, is assumed to be correct. The hardware (or software) implementation that must conform to this specification is to be verified.

параллельный алгоритмверификацияпараллельный автоматграф достижимых состоянийспецификация на проектированиеparallel algorithmverificationparallel automatongraph of reachable statesspecification for designРабота выполнена при финансовой поддержке БРФФИ (проект Ф17APM-008).This work was supported by the BRFFR (project F17APM-008).ReferencesВалидация на системном уровне. Высокоуровневое моделирование и управление тестированием : пер. с англ. Е. Б. Махияновой / М. Чэнь [и др.]. – М. : Техносфера, 2014. – 296 с.Chen M., Qin X., Koo H.-M., Mishra P. System-Level Validation High-Level Modeling and Directed Test Generation Techniques. New York, Springer-Verlag, 2013, 250 p.Tretmans, J. Model based testing with labelled transition systems / J. Tretmans // Formal Methods and Testing: Lecture Notes in Computer Science. – Springer, 2008. – Vol. 4949. – P. 1–38.Tretmans J. Model based testing with labelled transition systems. Formal Methods and Testing: Lecture Notes in Computer Science. Springer, 2008, vol. 4949, pp. 1–38.Lee, D. Principles and methods of testing finite state machine – a survey / D. Lee, M. Yannakakis // Proceedings of the IEEE. – 1996. – Vol. 84, no. 8. – P. 1090–1123.Lee D., Yannakakis M. Principles and methods of testing finite state machine – a survey. Proceedings of the IEEE, 1996, vol. 84, no. 8, pp. 1090–1123.Верификация автоматных программ / С. Э. Вельдер [и др.]. – СПб. : Наука, 2011. – 244 с.Vel'der S. E., Lukin М. А., Shalyto А. А., Jaminov B. R. Verifikacija avtomatnyh program. Verification of Automation Programs. Saint Petersburg, Nauka, 2011, 244 p. (in Russian).Питерсон, Дж. Теория сетей Петри и моделирование систем : пер. с англ. М. В. Горбатовой, В. Л. Торхова, В. Н. Четверикова / Дж. Питерсон. – М. : Мир, 1984. – 264 с.Peterson J. Petri Net Theory and the Modeling of Systems. New York, Prentice Hall, 1981, 290 p.Котов, В. Е. Сети Петри / В. Е. Котов. – М. : Наука, 1984. – 160 с.Kotov V. Е. Seti Petri. Petri Nets. Мoscow, Nauka, 1984, 160 p. (in Russian).Karatkevich, A. Dynamic Analysis of Petri Net-based Discrete Systems / A. Karatkevich. – Berlin : Springer-Verlag, 2007. – Vol. 358. – 166 p.Karatkevich A. Dynamic Analysis of Petri Net-based Discrete Systems. Berlin, Springer-Verlag, 2007, vol. 358, 166 p.Закревский, А. Д. Параллельные алгоритмы логического управления / А. Д. Закревский. – Минск : Ин-т техн. кибернетики НАН Беларуси, 1999. – 202 с.Zakrevskij A. D. Parallel'nye algoritmy logicheskogo upravlenija. Parallel Algorithms of Logical Control. Minsk, Institut tehnicheskoj kibernetiki Nacional'noj akademii nauk Belarusi, 1999, 202 p. (in Russian).Hack, M. Analysis of production schemata by Petri nets / M. Hack // Project MAK-94. – Cambridge, 1972. – 119 р.Hack M. Analysis of production schemata by Petri nets. Project MAK-94, Cambridge, 1972,119 р.Experimental system of automated design of logical control devices / A. D. Zakrevskij [et al.] // Proc. of the Intern. Workshop "Discrete Optimization Methods in Scheduling and Computer-Aided Design". – Минск : Ин-т техн. кибернетики НАН Беларуси, 2000. – C. 216–221.Zakrevskij A. D., Pottosin Yu. V., Vasilkova I. V., Romanov V. I. Experimental system of automated design of logical control devices. Proceedings of the International Workshop "Discrete Optimization Methods in Scheduling and Computer-Aided Design". Minsk, Institut tehnicheskoj kibernetiki Nacional'noj akademii nauk Belarusi, 2000, pp. 216–221.Романов, В. И. Разработка инструментальных средств логического проектирования / В. И. Романов // Логическое проектирование. – Минск : Ин-т техн. кибернетики НАН Беларуси, 2001. – Вып. 6. – С.151–170.Romanov V. I. Razrabotka instrumental'nyh sredstv logicheskogo proektirovayija [Development of Instruments for Logical Design]. Logicheskoe proektirovanie.Vyp. 6 [Logical Design. Issue 6]. Minsk, Institut tehnicheskoj kibernetiki Nacional'noj akademii nauk Belarusi, 2001, pp. 151–170 (in Russian).Thimbleby, H. The directed Chinese Postman Problem / H. Thimbleby // Software Practice and Experience. – 2003. – Vol. 33, no. 11. – P. 1081–1096.Thimbleby H. The directed Chinese Postman Problem. Software Practice and Experience, 2003, vol. 33, no. 11, pp. 1081–1096.Бурдонов, И. Б. Неизбыточные алгоритмы обхода ориентированных графов. Детерминированный случай / И. Б. Бурдонов, А. С. Косачев, В. В. Кулямин // Программирование. – 2003. – № 5. – С. 11–30.Burdonov I. B, Kosachev A. S., Kuljamin V. V. Neizbytochnye algoritmy obhoda orientirovannyh grafov. Determinirovannyj sluchaj [Irredandant algorithms for traversal of directed graphs. The determinate case]. Programmirovanie [Programming], 2003, no. 5, pp. 11–30 (in Russian).Черемисинова, Л. Д. Построение тестов полного перебора для оценки энергопотребления последовательностных схем / Л. Д. Черемисинова // Информатика. – 2017. – № 4. – С. 104–110.Cheremisinova L. D. Postroenie testov polnogo perebora dlja ocenki energopotreblenija posledovatel'nostnyh shem [Constructing tests of exhaustive search for estimation of power consumption of sequential circuits]. Informatika [Informatics], 2017, no. 4, pp. 104–110 (in Russian).Kanso, B. Compositional testing for FSM-based models / B. Kanso, O. Chebaro // Intern. J. of Software Engineering & Applications (IJSEA). – 2014. – Vol. 5, no. 3. – Р. 1–20.Kanso B., Chebaro O. Compositional testing for FSM-based models. International Journal of Software Engineering & Applications (IJSEA), 2014, vol. 5, no 3, рр. 1–20.Витязь, К. А. Алгоритмы построения функциональных тестов для цифровой схемы на основе автоматной модели ее поведения / К. А. Витязь, В. И. Романов // Танаевские чтения : доклады Восьмой Междунар. науч. конф., Минск, 27–30 марта 2018 г. – Минск : ОИПИ НАН Беларуси, 2018. – C. 52–56.Vitjaz' K. A., Romanov V. I. Algoritmy postroenija funkcional'nyh testov dlja cifrovoj shemy na osnove avtomatnoj modeli ejo povedenija [Algorithms for constructing functional tests for a digital circuit on the base of automaton model of its behavior]. Tanaevskie chtenija: doklady Vos'moj Mezhdunarodnoj nauchnoj konferencii [Tanaev Lecturings: Proceedings of the Eighth International Scientific Conference, Minsk, 27–30 March 2018], Minsk, Ob''edinennyj institut problem informatiki Nacional'noj akademii nauk Belarusi, 2018, pp. 52–56 (in Russian).

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