Research Of System Security Verification Technology Combined With Testing

Nowadays, the technique of verification and testing are learning from each other in mutual emulation and do their best to improve the safety, reliability of the sofeware. One kind of verification approach which called model checking now can be used in testing, and the conformance conclusion which derive from testing now can be used to improve verification and make it more perfect. So testing and verification are playing a complementary role in the approach of validation, and will be getting more and more closer in the future. This thesis starts with analysing the existence defects of ioco conformance, then successfully working out the system safety problems which aroused by limitation of the testing, through the use of software model checking approach. To complete this work, the following several aspects of the research work mainly have been done:First:Research on the two kinds of defects which arouse from ioco conformance, and given the definition of volating the system safety properties; Second:Introducing the SDR algorithms which can be used for finding out the problems of system safety problem; Third:Work out the problem, by using the different ways to deal with different traces which has been find out and been classified as two kinds of traces. Durning the experimental phase, the methodology which has been mentionec above are used to analyse the simulation software of ATM, and show how it works with the example of coffee machine.