Web交互模型的形式化验证研究  

Research on Formal Verification of Web Interaction Model

作　　者：李敏[1] 罗惠琼[2] 唐春玲[1] 王强[2] 

机构地区：[1]重庆广播电视大学电子信息工程学院,重庆400052 [2]电子科技大学计算机科学与工程学院,成都611731

出　　处：《计算机科学》2014年第2期219-221,共3页Computer Science

基　　金：重庆市教委(kj131607)资助

摘　　要：Web交互模型的形式化验证是对Web事件属性进行校验的十分可信的方法。通过一系列的系统模型建立、系统行为分析以及对于模型中关心属性的相关验证,能够让交互模型在设计阶段就能使形式化模型暴露出其所存在的缺陷,而不至于让缺陷保留到编码阶段或者更后面才能被真正地暴露出来,这样使系统模型的生存能力更加强大,同时避免了因后期缺陷暴露而出现的大代价修复。通过对Web系统的交互应用服务的过程模型化的体系进行研究,通过模型本身具有的属性进行相关正确性的校验,主要通过使用数学推理实现系统逻辑上的服务交互进程,从而进行过程的推演,并对系统服务的正确性进行过程的形式化验证,从而使系统服务模块的属性正确性可以通过逻辑上的演进来发现服务问题的存在,而不再是系统通过编码实现后才发现。对Web交互模型的形式化验证是基于IMWSC模型语义形成的IMWSC模型的验证机制。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. Be- sides,process modeling achieves service interaction processes deduction on system logic unit through mathematical rea- soning. And formal verification of process aiming at the correctness of system services was also performed. The advan- tage 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.

关 键 词：Web交互模型 形式化验证 数理推演 模型语义 

分 类 号：TP317.4[自动化与计算机技术—计算机软件与理论]