Verification of systems with behavior parallelism on the basis of the graph of reachable states
Abstract
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.
Keywords
parallel algorithm,
verification,
parallel automaton,
graph of reachable states,
specification for design
Supporting agencies: This work was supported by the BRFFR (project F17APM-008).
About the Authors
Yu. V. Pottosin
The United Institute of Informatics Problems of the National Academy of Sciences of Belarus
Belarus
Belarus
Yuri V. Pottosin, Cand. Sci. (Phys.-Math.), Leading Researcher
V. I. Romanov
The United Institute of Informatics Problems of the National Academy of Sciences of Belarus
Vladimir I. Romanov, Cand. Sci. (Eng.), Leading Researcher
Vladimir I. Romanov, Cand. Sci. (Eng.), Leading Researcher
L. D. Cheremisinova
The United Institute ofInformatics Problems of the National Academy of Sciences of Belarus
Ljudmila D. Cheremisinova, Dr. Sci. (Eng.), Chief Researcher
Ljudmila D. Cheremisinova, Dr. Sci. (Eng.), Chief Researcher
References
1. 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.
2. 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.
3. 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.
4. Vel'der S. E., Lukin М. А., Shalyto А. А., Jaminov B. R. Verifikacija avtomatnyh program. Verification of Automation Programs. Saint Petersburg, Nauka, 2011, 244 p. (in Russian).
5. Peterson J. Petri Net Theory and the Modeling of Systems. New York, Prentice Hall, 1981, 290 p.
6. Kotov V. Е. Seti Petri. Petri Nets. Мoscow, Nauka, 1984, 160 p. (in Russian).
7. Karatkevich A. Dynamic Analysis of Petri Net-based Discrete Systems. Berlin, Springer-Verlag, 2007, vol. 358, 166 p.
8. 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).
9. Hack M. Analysis of production schemata by Petri nets. Project MAK-94, Cambridge, 1972,119 р.
10. 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.
11. 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).
12. Thimbleby H. The directed Chinese Postman Problem. Software Practice and Experience, 2003, vol. 33, no. 11, pp. 1081–1096.
13. 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).
14. 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).
15. Kanso B., Chebaro O. Compositional testing for FSM-based models. International Journal of Software Engineering & Applications (IJSEA), 2014, vol. 5, no 3, рр. 1–20.
16. 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).
Review
For citations:
Pottosin Yu.V., Romanov V.I., Cheremisinova L.D. Verification of systems with behavior parallelism on the basis of the graph of reachable states. Informatics. 2019;16(2):62-72. (In Russ.)
Views: 653
Email this article 