Properties Description And Verification Of C Program Based On Specification Patterns

With the increase in the complexities of software and extension of their application areas, how to ensure software reliability becomes a hotspot question in the domain of software engineering. Software testing is used to find errors, but it can't prove program correctness. Formal Method is a good way to solve this problem, but formal description language is difficult to write for developers. In this paper, it proposes a semi-formal language C-PDL for describing properties of C program, which is based on Specification Patterns, and researches the conversion from C-PDL to input language of SPIN. The verification of C program against properties expressed in C-PDL by SPIN is also discussed.Specification Patterns are high-level abstractions of frequently used temporal logic formulae. Specification Patterns enable people who are not experts in temporal logics to read and write formal specifications. Because the semantic of Specification Patterns is inexplicit, the property can generate different LTL formulae, including SPS and Prospec. In this paper, it verifies LTL formulae in SPS by SPIN, and corrects the semantic of Specification Patterns to ensure the conformance between Specification Patterns and SPS.C program describes state transition, so its properties can be expressed in Specification Patterns. In order to make these properties clearer, the state is extended to include variable information and location information. C-PDL builds on Specification Patterns and adds a pattern for describing assertions, which is on the basis of extended state. It's able to describe dynamic properties of sequence program and concurrent program and the program's invariant. SPIN can't directly verify the properties expressed in C-PDL. So in this paper it researches the conversion from C-PDL to input language of SPIN.Based on all these works, in this paper it describes properties of alternating-bit and producer-consumer in C-PDL and verifies them by SPIN. This process can present the expression ability of C-PDL and prove that the conversion from C-PDL to input language of SPIN is right. This method not only can make C program right according to some properties, but also can expediently find errors.