The Study on Software Model Checking Technique for Security Detection in Code

摘要

This article describes how to use Bandera specification language to describe safety planning to guide temporal.logic features in two case studies. The first step of the project is with Java source model software Bandera to check whether safe programming guide, and thus for the corresponding security vulnerabilities exists. In case study, Bandera as tool software source code model reduce the programmer's extra effort as one target