基于xml的web应用模型抽取

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