|
Combination of static verification methods for checking requirements composition
V. O. Mordan Institute for System Programming of the Russian Academy of Sciences
Abstract:
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.
Keywords:
software model checking, counterexample guided abstraction refinement, reachability task, requirements composition.
Citation:
V. O. Mordan, “Combination of static verification methods for checking requirements composition”, Proceedings of ISP RAS, 29:3 (2017), 151–170
Linking options:
https://www.mathnet.ru/eng/tisp226 https://www.mathnet.ru/eng/tisp/v29/i3/p151
|
Statistics & downloads: |
Abstract page: | 135 | Full-text PDF : | 75 | References: | 33 |
|