Abstract: Formal verification of Web interaction model is a credible way on evaluating the attributes of Web events．Through a series of system modeling,behavior analysis,and related validation of center properties,defects will expose during the design phase instead of coding phase or later in the formal model．Thereby,the viability of system model is more powerful．At the mean time,it cost less than the spending of late defect exposure．We investigated the process modeling of interactive application service on Web system,checking the correctness of model’s relative properties．Besides,process modeling achieves service interaction processes deduction on system logic unit through mathematical reasoning．And formal verification of process aiming at the correctness of system services was also performed．The advantage of this method reflects mainly on the early discovery of defects in system service model．The formal verification of Web interaction model is based on IMWSC model verification mechanism.

Key words: Web interaction model,Formal Verification,Mathematical deduction,Model semantics