Research And Application Of Hardware Verification Based On Model Checking In Financial Field

The embedded product is more complex and its application has been made extensive use of in financial sector.But the stability of embedded product still remains ineffectively resolved.Thus,it will bring some potential concerns in daily financial transactions and even property loss.To solve this problem,the thesis analyzes and researches of peripheral controllers verification method based on model checking,to maximize the stability of embedded products.Firstly,current researches on hardware design verification testing and model checking will be described,and related technologies on hardware verification methods which include verification methodology analysis,verification of key technology based on SystemVerilog and model checking will be researched;Then researches of model verify models construction methods,including cases of model transform into a state model,the state model convert to nuSMV model and transformation rules between them;Next,the study of model checking model properties design methods which involve attribute extraction,decomposition and design approaches.Finally,case researches,which is based on practical development project that A class cash counting machine as a platform for the sensor & controller adopt case modeling,state modeling and nuSMV modeling on contact image to verify model and emerge error trace;with the continuously improvement for the sensor & controller compared to the error trace,to achieve the reliable sensor & controller for contact image.By using model checking verification method to complete the design for sensor & controller of contact image,the instability and poor quality problems of contact image sensor & controller are solved.Moreover,the model checking verification method will be more extensive applied in the hardware field.