摘要
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.
出处
《计算机科学》
CSCD
北大核心
2014年第2期219-221,共3页
Computer Science
基金
重庆市教委(kj131607)资助
关键词
Web交互模型
形式化验证
数理推演
模型语义
Web interaction model, Formal Verification, Mathematical deduction, Model semantics
