计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2011年
9期
130-134,149
,共6页
程广金%缪淮扣%方明科%梅佳%高洪皓
程廣金%繆淮釦%方明科%梅佳%高洪皓
정엄금%무회구%방명과%매가%고홍호
XML文档%时间约束%模型抽取%时间自动机
XML文檔%時間約束%模型抽取%時間自動機
XML문당%시간약속%모형추취%시간자동궤
以模型检验为目标,从时间的约束角度出发,提出一种基于XML文档的Web应用的模型抽取方法.模型抽取由时间及相关链接的提取、模型构造和结果显示3部分组成.首先,通过对Web应用进行逆向分析,从带时间约束的XML源代码对链接及时间约束等相关信息进行提取、规整和存储.其次,对Web应用中的链接、时间约束等建模元素进行分析,应用映射与聚合等抽象技术对获得的信息进行重构,得到适合于形式化验证的时间自动机(TA,Timed Automata)模型,并对时间约束下的并发进行模型组合.最后,以电子邮箱系统为实例阐述如何实现模型抽取.
以模型檢驗為目標,從時間的約束角度齣髮,提齣一種基于XML文檔的Web應用的模型抽取方法.模型抽取由時間及相關鏈接的提取、模型構造和結果顯示3部分組成.首先,通過對Web應用進行逆嚮分析,從帶時間約束的XML源代碼對鏈接及時間約束等相關信息進行提取、規整和存儲.其次,對Web應用中的鏈接、時間約束等建模元素進行分析,應用映射與聚閤等抽象技術對穫得的信息進行重構,得到適閤于形式化驗證的時間自動機(TA,Timed Automata)模型,併對時間約束下的併髮進行模型組閤.最後,以電子郵箱繫統為實例闡述如何實現模型抽取.
이모형검험위목표,종시간적약속각도출발,제출일충기우XML문당적Web응용적모형추취방법.모형추취유시간급상관련접적제취、모형구조화결과현시3부분조성.수선,통과대Web응용진행역향분석,종대시간약속적XML원대마대련접급시간약속등상관신식진행제취、규정화존저.기차,대Web응용중적련접、시간약속등건모원소진행분석,응용영사여취합등추상기술대획득적신식진행중구,득도괄합우형식화험증적시간자동궤(TA,Timed Automata)모형,병대시간약속하적병발진행모형조합.최후,이전자유상계통위실례천술여하실현모형추취.
