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 shoul...

Full description

Bibliographic Details
Main Author: V. O. Mordan
Format: Article
Language:English
Published: Ivannikov Institute for System Programming of the Russian Academy of Sciences 2018-10-01
Series:Труды Института системного программирования РАН
Subjects:
Online Access:https://ispranproceedings.elpub.ru/jour/article/view/282
Description
Summary: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.
ISSN:2079-8156
2220-6426