Combination of static verification methods for checking requirements composition

Бесплатный доступ

Static verification proves correctness of the software against checked requirements, but it requires a lot of resources for that and its task is undecidable in general case. At present there is no universal static verification method, which could efficiently check any software. That is why one should choose more appropriate method and set its parameters for checking correctness of the given requirements in a given program. This paper suggests to combine different static verification methods in order to increase efficiency and effectiveness of verification, which is the first step in creating universal method for static verification. The suggested methods were implemented as combination of actively developing static verification methods for checking requirements composition. Implementation of the suggested methods showed their advantages on Linux kernel modules in comparison with using of each verification method separately.

Еще

Software model checking, counterexample guided abstraction refinement, reachability task, requirements composition

Короткий адрес: https://sciup.org/14916433

IDR: 14916433   |   DOI: 10.15514/ISPRAS-2017-29(3)-9

Статья научная