基于XML的Web应用模型抽取

Extracting Model of Web Application Based on XML

以模型检验为目标,从时间的约束角度出发,提出一种基于XML文档的Web应用的模型抽取方法。模型抽取由时间及相关链接的提取、模型构造和结果显示3部分组成。首先,通过对Web应用进行逆向分析,从带时间约束的XML源代码对链接及时间约束等相关信息进行提取、规整和存储。其次,对Web应用中的链接、时间约束等建模元素进行分析,应用映射与聚合等抽象技术对获得的信息进行重构,得到适合于形式化验证的时间自动机(TA,Timed Automata)模型,并对时间约束下的并发进行模型组合。最后,以电子邮箱系统为实例阐述如何实现模型抽取。

For model checking,an approach to extracting TA models of Web application based on XML document with time constraint was proposed.The extraction process is divided into three phases：time and link extraction,model construction and display.Firstly,analyzed Web application reversely to extract,structure and store information related to link and time constraint from XML source code.Then,analyzed elements for model construction such as link and time constraint,and restructure the information obtained with mapping and aggregation technology.Finally the TA（Timed Automata） model applying for formal checking was obtained.A particular case study,a mail box system is taken to illustrate the method to be feasible.