D. S. Chivilikhin, V. I. Ulyantsev, V. V. Vyatkin, A. A. Shalyto

Read the full article  ';
Article in Russian

The procedure of testing traditionally used in software engineering cannot guarantee program correctness; therefore verification is used at the excess requirements to programs reliability. Verification makes it possible to check certain properties of programs in all possible computational states; however, this process is very complex. In the model checking method a model of the program is built (often, manually) and requirements in terms of temporal logic are formulated. Such temporal properties of the model can be checked automatically. The main issue in this framework is the gap between the program and its model. Automata-based programming paradigm gives the possibility to overcome this limitation. In this paradigm, program logic is represented using finite-state machines. The advantage of finite-state machines is that their models can be constructed automatically. The paper deals with the application of mutation-based ant colony optimization algorithm to the problem of finite-state machine construction from their specification, defined by test scenarios and temporal properties. The presented approach has been tested on the elevator doors control problem as well as on randomly generated data. Obtained results show the ant colony algorithm is two-three times faster than the previously used genetic algorithm. The proposed approach can be recommended for inferring control programs for critical systems.

Keywords: finite-state machine, ant colony algorithm, verification

Acknowledgements. The work is partially financially supported by the Government of the Russian Federation (grant 074-U01), and also partially supported by RFBR (scientific project № 14-07-31337 мол_а).

 1.     Clarke E.M., Grumberg O., Peled D.A. Model Checking. MIT press, 1999, 330 p.
2.     Polikarpova N.I., Shalyto A.A. Avtomatnoe Programmirovanie [Automata Programming]. St. Petersburg, Piter Publ., 2009, 176 p.
3.     Egorov K.V., Tsaryov F.N., Shalyto A.A. Primenenie geneticheskogo programmirovaniya dlya postroeniya avtomatov upravleniya sistemami so slozhnym povedeniem na osnove obuchayushchikh primerov i spetsifikatsii [Application of genetic programming and model checking for finite-state machine induction on the base of tests and specification]. Scientific and Technical Journal of Information Technologies, Mechanics and Optics, 2010, no. 5 (69), pp. 81–86.
4.     Tsarev F., Egorov K. Finite state machine induction using genetic algorithm based on testing and model checking. Proc. 13th Annual Genetic and Evolutionary Computation Conference, GECCO'11. Dublin, Ireland, 2011, pp. 759–762. doi: 10.1145/2001858.2002085
5.     Yang C.-H., Vyatkin V., Pang C. Model-driven development of control software for distributed automation: a survey and an approach. IEEE Transactions on Systems, Man, and Cybernetics: Systems, 2014, vol. 44, no. 3, pp. 292–305. doi: 10.1109/TSMCC.2013.2266914
6.     Chivilikhin D., Ulyantsev V. MuACOsm – a new mutation-based ant colony optimization algorithm for learning finite-state machines. Proc. 15th Genetic and Evolutionary Computation Conference, GECCO 2013. Amsterdam, Netherlands, 2013, pp. 511–518. doi: 10.1145/2463372.2463440
7.     Chivilikhin D.S. Ulyantsev V.I., Shalyto A.A. Murav'inyi algoritm dlya postroeniya avtomatnykh programm po spetsifikatsii [Ant algorithm for construction of automata on the specification]. Trudy XII Vserossiiskogo Soveshchaniya po Problemam Upravleniya VSPU-2014 [Proc. XII National Conference on Control, VSPU 2014]. Moscow, 2014, pp. 4531–4542.
8.     Egorov K.V. Generatsiya upravlyayushchikh konechnykh avtomatov na osnove geneticheskogo programmirovaniya i verifikatsii. Dis. kand. tekhn. nauk. [Generating control of finite state machines based on genetic programming and verification. Dis. eng. sci.]. St. Petersburg, NRU ITMO, 2013, 150 p.
9.     Vel'der S.E., Lukin M.A., Shalyto A.A., Yaminov B.R. Verifikatsiya Avtomatnykh Programm [Verification of Automata Programs]. St. Petersburg, Nauka Publ., 2011, 244 p.
10.Ul'yantsev V.I. Postroenie upravlyayushchikh konechnykh avtomatov po stsenariyam raboty na osnove resheniya zadachi udovletvoreniya ogranichenii. Magisterskaya dissertatsiya [Construction of finite automata for scenarios control on the basis of solving constraint satisfaction problems. Master dissertation]. Available at: (accessed 30.09.2014).
11.Skobtsov Yu.A., Fedorov E.E. Metaevristiki [Metaheuristics]. Donetsk, NOULIDZh Publ., 2013, 426 p.
12.Dorigo M., Stutzle T. Ant Colony Optimization. MIT Press, 2004, 319 p.
13.Lopez-Ibanez M., Dubois-Lacoste J., Stutzle T., Birattari M. The irace package: iterated race for automatic algorithm configuration. Technical Report TR/IRIDIA/2011-004. IRIDIA, Belgium, 2011, 20 p.
14.Wilcoxon F. Probability tables for individual comparisons by ranking methods. Biometrics, 1947, vol. 3, pp. 119–122.

Creative Commons License

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License
Copyright 2001-2021 ©
Scientific and Technical Journal
of Information Technologies, Mechanics and Optics.
All rights reserved.