Menu
Publications
2024
2023
2022
2021
2020
2019
2018
2017
2016
2015
2014
2013
2012
2011
2010
2009
2008
2007
2006
2005
2004
2003
2002
2001
Editor-in-Chief
Nikiforov
Vladimir O.
D.Sc., Prof.
Partners
AUTOMATA PROGRAMS CONSTRUCTION FROM SPECIFICATION WITH AN ANT COLONY OPTIMIZATION ALGORITHM BASED ON MUTATION GRAPH
Read the full article ';
Article in Russian
Abstract
Abstract
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 мол_а).
References
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 мол_а).
References
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: http://is.ifmo.ru/diploma-theses/2013/master/ulyantsev/ulyantsev.pdf (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.