Abstract: Model checking is an effective formal method that provides rigorous assurance of software quality. A workflow is given to describe the sourceoriented software model checking method. To solve the specification describing problem, a specification language is proposed, which is independent of the source code. Its syntax is easy to use and is compliant with the habits of programmers. Based on the path traversal of programcontrol flow graph, a lightweight model checking method is proposed to support functions verification, interfunctions verification and specification checking.

Key words: software analysis, formal methods, model checking, program verification, predicate abstraction