RUS  ENG
Full version
JOURNALS // Proceedings of the Institute for System Programming of the RAS // Archive

Proceedings of ISP RAS, 2017 Volume 29, Issue 3, Pages 151–170 (Mi tisp226)

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.

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



Bibliographic databases:


© Steklov Math. Inst. of RAS, 2024