Artificial intelligence

Abstract: A method of symbolic modeling of formal models is considered in the paper. Object of analysis is a domain of multi-component concurrent systems specified in basic protocols language. A problem of dynamic creation and stopping of agents during state-space exploration is considered. Corresponding algorithm has been suggested as an extension of existing forward and backward predicate transformers. It provides ability to introduce arbitrary number of concurrent processes in verification and test generation.

Keywords: symbolic modeling, state-space, concurrent systems

References:

1. Hoare C. A. R. An axiomatic basis for computer programming // Communications of the ACM. – 1969. – Vol. 12(10). – P. 576–585.
2. A. Letichevsky, J. Kapitonova, V. Volkov, A. Letichevsky Jr., S. Baranov, V. Kotlyarov, T. Weigert. Specification of systems using basic protocols // Cybernetics and System Analysis. – 2005. – N 4. – P. 3–21. (in Russian)
3. Amir Pnueli, Ofer Strichman. Reduced Functional Consistency of Uninterpreted Functions // Electronic Notes in Theoretical Computer Science (ENTCS). – 2006. – Vol. 144. – Issue 2. – P. 53–65.
4. Potiyenko S. Methods of forward and backward symbolic modeling of systems specified by basic protocols // Problems in Programming. – 2008. – № 4. – P. 39–45. (in Russian)
5. Godlevsky A., Potiyenko S. Backward transformation of formulas in symbolic modeling: from the result to the source formula // Problems in Programming. – 2010. – N 2–3. – P. 363–368. (in Russian)
6. Letichevsky A., Godlevsky A., Letychevskyy O.(jr.), Potiyenko S., Peschanenko V. Properties of VRS predicate transformer // Cybernetics and System Analysis. – 2010. – Volume 46. – P. 521–532. (in Russian)
7. A. Kolchin, A. Letichevsky, V. Peschanenko, P. Drobintsev, V. Kotlyarov. An approach to test scenarios concretization in scope of test automation technology of industrial software projects // Modeling and Analysis of Information Systems. Yaroslavskiy National University named after P.G. Demidov. – 2012. – N 6. – P. 79–91.
8. A. Kolchin, V. Kotlyarov, P. Drobintsev. A method of test scenarios generation in insertion modeling environment // Control Systems and Computers. – 2012. – N 6. – P. 43-48.