Штучний інтелект

Анотація: The core of the proposed method is an algorithm for cutting of formal model behavior branches, which are redundant with respect to verified properties. The fact of redundancy is derived basing on proof of isomorphism on the model’s informational dependency graph. In many cases, such approach significantly reduces «state space combinatorial explosion» effect.

Ключові слова: model checking, state space reduction

Посилання:

1. Karpov Y.G. Model Checking. – BHV-Petersburg. – 2010. – 552 P.
2. Jhala R., Majumdar R. Software model checking // ACM Comput. Surv. – Vol.41(4). – 2009. – 54 P.
3. Peled D. Partial order reduction: linear and branching temporal logics and process algebras // In proc. of the workshop on Partial order methods in verification. NY, USA: AMS Press, Inc. – 1997. – P. 233–257.
4. Godefroid P. Partial-order methods for the verification of concurrent systems – an approach to the state– explosion problem // LNCS, Springer-Verlag. – 1996. – Vol. 1032. –143 P.
5. Holzmann G., Peled D. An improvement in formal verification // FORTE Conf. – 1994. – P. 197-211.
6. Kolchin A.V. An automatic method for the dynamic construction of abstractions of states of a formal model // Cybernetics and system analysis. – 2010. – № 4. – P. 70-90.
7. Holzmann G. The model checker SPIN // IEEE transactions. – 1997. – Vol. 23. – N 5. – P. 279–295.
8. Dijkstra E. Guarded commands, nondeterminacy and formal derivation of programs // Communications of the ACM. – 1975. – Vol.18. – N 8. – P. 453–457.
9. Kolchin A.V. Enabled transitions detection optimization in formal model verification // Problems in programming. – 2012. – №2–3. – P. 201–210.
10. Podgurski A., Clarke A.A. Formal model of program dependencies and its implications for software testing, debugging and maintenance // IEEE Trans. Software Eng. – 1990. – Vol. 16(9). – P. 965-979.
11. Ottenstain K.J., Ottenstain L.M. The program dependence graph in a software development environment // In proc. of the ACM SIGSOFT/SIGPLAN software engineering symposium on practial software development environments. –1984. –V.19(5). –P.177–184.
12. Cortesi A., Halder R. Dependence Condition Graph for Semantics-based Abstract Program Slicing // In Proc. of the 10th Workshop on Language Descriptions, Tools and Applications. – 2010. – № 4. – 9 P.
13. Tip F. A survey of program slicing techniques // Technical report. Centre for Mathematics and Computer Science, Amsterdam, The Netherlands. –1994. – 65 P.
14. Wilander J. Modeling and visualizing security properties of code using dependence graphs // In Proc. of the 5th Conference on Software Engineering Research and Practice in Sweden. – 2007. – P. 65–74.
15. Krinke J. Program Slicing // In Handbook of software engineering and knowledge engineering. – 2005. – Vol. 3.– P. 307–332.
16. Ilan Beer, Shoham Ben-David and oth. Explaining Counterexamples Using Causality // Formal Methods in System Design. – 2012. – №40. – P. 20-40.
17. Kolchin A., Chetvertak R. An interactive system for analysis of formal models behavior. –2012. – № 4. – P. 330-341.
18. Holzmann G. An analysis of bitstate hashing // Formal Methods in Systems Design. – 1998. – P.301-314.
19. Clarke E., Grumberg O., Jha S., and oth. Counterexample-guided abstraction refinement for symbolic model checking // Journal of the ACM. –2003. – Vol. 50. – № 5. – P. 752-794.