Program Validation Tool Based On Slice

A large number of software project developments show that costs of software development are mostly spent in correcting various errors which are found in testing. And these errors are caused by inaccurate description in the phase of demand analysis. In order to overcome the defects of demand description written by natural language and programming language,formal methods were proposed.Formalized method describes and validates the characters of aimed software system with mathematical tools.It usually uses formalized specification languages to describe software requirement.Model checking technology is a form of verification methods.SPIN is a common model checking tool and it uses PROMELA as input statement.PROMELA language requires sending and receiving information,its grammar form is abstract and requires a strong mathematical foundation and the basis of program design.Because specification of the software described by mathematic symbols is abstract and non-executable,non-professionals can't understand and estimate it easily.The project topic is the design and realization of program validation tool based on slice.By researching the internal principle and application of the software model checking technology,we hope non-professionals can also use formalized method to test and verify abstract design models.We also developed project supporting tool - C2P.,which was written by C# language and developed by Visual Studio 2005.During the development process,I spent much time in studying PROMELA language,distinguishing between PROMELA and C# code,and using the slicing techniques.By analyzing the context of C # code,we tried to find its impact statement and control predicate,do back slice,translate and compile.We also studied lexical analysis and syntax analysis of C# and finally transferred the slice to corresponding PROMELA language.C2P basically realized the function of transferring the C# code to PROMELA directly.By using friendly form interface,non-professionals can use simple selections, clicks and other operations to achieve model checking by SPIN.