Combination of static verification methods for checking requirements composition
https://doi.org/10.15514/ISPRAS-2017-29(3)-9
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.
About the Author
V. O. Mordan
Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Russian Federation
References
1. Turing A. M. On Computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, 1936, pp. 230-265.
2. Corbet J., Kroah-Hartman G., McPherson A. Linux kernel development. How Fast it is Going, Who is Doing It, What They are Doing, and Who is Sponsoring It. Доступно по ссылке: https://www.linux.com/publications/linux-kernel-development-how-fast-it-going-who-doing-it-what-they-are-doing-and-who-5, свободный, 2016.
3. Mutilin V.S., Novikov E.M., Khoroshilov A.V. Analysis of typical faults in Linux operating system drivers. Trudy ISP RAN / Proc. ISP RAS, vol. 22, 2012, pp. 349-374 (in Russian). DOI: 10.15514/ISPRAS-2012-22-19.
4. Mordan V., Novikov E. Minimizing the number of static verifier traces to reduce time for finding bugs in Linux kernel modules. Proceedings of 8th Spring/Summer Young Researchers Colloquium on Software Engineering, vol. 1, 2014. DOI: 10.15514/syrcose-2014-8-5.
5. Mordan V., Mutilin V. Checking several requirements at once by CEGAR. LNCS, vol. 9609, pp. 218-232, 2016. DOI: 10.1007/978-3-319-41579-6_17.
6. Mordan V. O., Mutilin V. S. Checking several requirements at once by CEGAR. Programming and Computer Software, vol. 42, no. 4, pp. 225-238, 2016. DOI: 10.1134/S0361768816040058.
7. Apel S., Beyer D., Mordan V., Mutilin V., Stahlbauer A. On-The-Fly Decomposition of Specifications in Software Model Checking. Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 349-361, 2016. DOI: 10.1145/2950290.2950349.
8. Beyer D., Henzinger T. A., Keremoglu M. E., Wendler P. Conditional model checking: a technique to pass information between verifiers. Proceedings ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering (FSE 2012), article 57, 2012. DOI: 10.1145/2393596.2393664.
9. Novikov E. M. Development of a contract specification method for verification of Linux kernel modules. PhD thesis. ISP RAS, 2013 (in Russian).
10. Beyer D., Chlipala A., Henzinger T. A., Jhala R., Majumdar R. The BLAST query language for software verification. Proceedings of SAS. LNCS, vol. 3148, pp. 2-18, 2004. DOI: 10.1007/978-3-540-27864-1_2.
11. Clarke E., Grumberg O., Jha S., Lu Y., Veith H. Counterexample-guided abstraction refinement. Proceedings of CAV, LNCS, vol. 1855, pp. 154-169, 2000. DOI: 10.1007/10722167_15.
12. Beyer D. Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2016). Proceedings of TACAS. LNCS, vol. 9636, pp. 887-904, 2016. DOI: 10.1007/978-3-662-49674-9_55.
13. Beyer D., Henzinger T., Jhala R., Majumdar R. The software model checker BLAST. International Journal on Software Tools for Technology Transfer, vol. 9, issue 5, pp. 505-525, 2007. DOI: 10.1007/s10009-007-0044-z.
14. Beyer D., Keremoglu M. CPAchecker: A tool for configurable software verification. Proceedings of Computer Aided Verification. LNCS, vol. 6806, pp. 184-190, 2011. DOI: 10.1007/978-3-642-22110-1_16.
15. Khoroshilov A., Mutilin V., Novikov E., Shved P., Strakh A. Towards an open framework for C verification tools benchmarking. Perspectives of Systems Informatics. LNCS, vol. 7162, pp. 179-192, 2012. DOI: 10.1007/978-3-642-29709-0_17.
16. Ball T., Rajamani S. K. The SLAM project. Debugging system software via static analysis. Proceedings of Symposium on Principles of Programming Languages (POPL), pp. 1-3, 2002. DOI: 10.1145/565816.503274.
17. Mordan V. O. Methods of software verification based on composition of reachability tasks. PhD thesis. ISP RAS, 2017 (in Russian).
18. Beyer D., Wendler P. Reuse of verification results. Proceedings of the 20th International Workshop on Model Checking Software (SPIN 2013). LNCS, vol. 7976, pp. 1-17, 2013. DOI: 10.1007/978-3-642-39176-7_1.
19. Beyer D., Keremoglu M., Wendler P. Predicate abstraction with adjustable-block encoding. Proceedings of Formal Methods in Computer-Aided Design, pp. 189-198, 2010.
20. Beyer D., Löwe S. Explicit-state software model checking based on CEGAR and interpolation. Proceedings of the 16th International Conference on Fundamental Approaches to Software Engineering (FASE 2013). LNCS, vol. 7793, pp. 146-162, 2013. DOI: 10.1007/978-3-642-37057-1_11.
Review
For citations:
Mordan V.O. Combination of static verification methods for checking requirements composition. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(3):151-170. (In Russ.) https://doi.org/10.15514/ISPRAS-2017-29(3)-9
Email this article 