Verification For System Reliability And Security Using Mdel Checking

With the development of computer technology,the reliability and security of systems have become the focus of attention.At present,in order to ensure the reliability and security of systems,testing and simulation technology are usually used.However,testing and simulation can only analyze a part of behavior of a system and it is difficult to find some hidden system defects.So we use model checking technology to verify systems in this paper.At present,a large number of model checking research has been applied in various fields,but it is still hard to completely replace testing and simulation.On the one hand,model checking is a model-based method and the construction of a model is important.Current computer systems are becoming more and more large and system models can easily cause the explosion of state space in a verification process.On the other hand,theories of model checking is complex,the specification and modeling methods are various,and model checking tools used for verification are mostly not universal.So it is necessary to spend a lot of time to learn about model checking.As a result,it has to some extent hindered the popularization of model checking.In this paper,we first use model checking to analyze routing protocols.In order to simplify the analysis of protocols,we propose an abstract description method to describe complex network protocols,keep property-related behaviors and remove redundant parts to reduce the system size.Then,based on two protocols,three different properties are proposed and the reliability and security are verified respectively.These two protocols represent small-scale network protocols and large-scale network protocols.The verification includes internal design flaws and external attacks which can prove the applicability of our method in routing protocols.In order to solve the shortcomings of manual modeling,we developed a model conversion tool to automatically convert C language programs to target verification models.We also analyze ARINC-653 as an example to illustrate the availability of this tool.