本文關(guān)鍵詞：基于CEGAR的Web應(yīng)用驗證

  更多相關(guān)文章： Web應(yīng)用 導(dǎo)航模型 抽象精化 模型檢驗 偽反例

【摘要】：Web應(yīng)用導(dǎo)航行為的建模和驗證是可信Web工程研究的重點和難點.在深入分析用戶和Web瀏覽器交互行為的基礎(chǔ)上,文中引入On-the-fly策略并基于反例引導(dǎo)的抽象精化驗證方法 CEGAR對Web應(yīng)用的導(dǎo)航行為進行建模和驗證.在On-the-fly導(dǎo)航模型展開的過程中,根據(jù)檢驗性質(zhì)采用增量式狀態(tài)抽象方法構(gòu)造Web應(yīng)用導(dǎo)航抽象模型,通過確認抽象反例來識別偽反例,借助等價類精化方法消除抽象模型上的偽反例.這一方法可有效地緩解Web應(yīng)用驗證過程中出現(xiàn)的狀態(tài)爆炸問題.
【作者單位】： 上海大學(xué)計算機工程與科學(xué)學(xué)院;上海大學(xué)計算中心;上海市計算機軟件評測重點實驗室;
【關(guān)鍵詞】： Web應(yīng)用 導(dǎo)航模型 抽象精化 模型檢驗 偽反例
【基金】：國家自然科學(xué)基金(61170044,61073050,61262010)資助~~
【分類號】：TP393.09
【正文快照】： 男,1985年生,博士,講師,中國計算機學(xué)會(CCF)會員,研究方向為模型檢驗、Web應(yīng)用、服務(wù)計算.E-mail:gaohonghao@shu.edu.cn.1引言互聯(lián)網(wǎng)的快速發(fā)展使得通過Web求解問題和開展業(yè)務(wù)逐漸成為電子商務(wù)的主流趨勢.越來越多的企業(yè)、單位、甚至個人都紛紛開始部署Web應(yīng)用程序和云計算

【參考文獻】

中國期刊全文數(shù)據(jù)庫 前4條

1 趙會群;孫晶;魏瑩;王文文;郭峰;;基于模型的網(wǎng)構(gòu)軟件可達性檢測方法研究[J];計算機學(xué)報;2011年06期

2 文艷軍;王戟;齊治昌;;并發(fā)反應(yīng)式系統(tǒng)的組合模型檢驗與組合精化檢驗[J];軟件學(xué)報;2007年06期

3 曾紅衛(wèi);繆淮扣;;構(gòu)件組合的抽象精化驗證[J];軟件學(xué)報;2008年05期

4 何炎祥;吳偉;陳勇;徐超;;基于SMT求解器的路徑敏感程序驗證[J];軟件學(xué)報;2012年10期

【共引文獻】

中國期刊全文數(shù)據(jù)庫 前10條

1 李秀娟;;構(gòu)件技術(shù)在ERP系統(tǒng)中的應(yīng)用[J];電子科技;2011年10期

2 張廣泉;戎玫;朱雪陽;何亞麗;石慧娟;;基于XYZ/ADL的Web服務(wù)組合描述與驗證[J];電子學(xué)報;2011年S1期

3 屈婉霞;龐征斌;郭陽;李暾;楊曉東;;參數(shù)化系統(tǒng)二維抽象框架[J];國防科技大學(xué)學(xué)報;2010年01期

4 秦浩;張學(xué)宏;;導(dǎo)引頭控制軟件的一種測試設(shè)計方法[J];航空計算技術(shù);2008年04期

5 林苗;戎玫;張廣泉;;基于構(gòu)件的嵌入式實時軟件組合時間分析研究[J];計算機工程與應(yīng)用;2009年11期

6 張馳;;基于角色劃分的構(gòu)件組合兼容性檢查[J];計算機工程與應(yīng)用;2010年05期

7 龐征斌;屈婉霞;郭陽;楊曉東;;參數(shù)化系統(tǒng)二維抽象的理論基礎(chǔ)[J];計算機科學(xué);2011年04期

8 王昌達;華明輝;周從華;宋香梅;鞠時光;;基于抽象和搜索空間劃分的安全性判定方法[J];計算機科學(xué);2011年10期

9 陳國彬;任強;張廣泉;;一種基于抽象與精化技術(shù)的Web服務(wù)組合驗證方法[J];計算機工程與科學(xué);2011年09期

10 丁佐華;江明月;劉靜;;基于常微分方程的死鎖檢測實驗分析[J];計算機學(xué)報;2009年09期

中國博士學(xué)位論文全文數(shù)據(jù)庫 前6條

1 劉銘;列車通信網(wǎng)絡(luò)系統(tǒng)形式化建模與驗證方法研究[D];哈爾濱工程大學(xué);2011年

2 曾紅衛(wèi);Web應(yīng)用的驗證與測試方法研究[D];上海大學(xué);2008年

3 伍建q;網(wǎng)構(gòu)軟件系統(tǒng)構(gòu)建的形式化分析研究[D];上海交通大學(xué);2009年

4 金洋;基于傳遞系統(tǒng)模型的在軌衛(wèi)星故障診斷方法研究[D];哈爾濱工業(yè)大學(xué);2013年

5 劉智;二進制代碼級的漏洞攻擊檢測研究[D];電子科技大學(xué);2013年

6 駱超;混沌和異步布爾網(wǎng)絡(luò)中若干問題的研究[D];大連理工大學(xué);2013年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前9條

1 馬偉民;基于組件技術(shù)的人機界面（HMI）研究[D];杭州電子科技大學(xué);2009年

2 陳卓;面向軟件復(fù)用的組件形式化開發(fā)[D];河南科技大學(xué);2010年

3 任強;基于謂詞抽象與精化技術(shù)的Web服務(wù)驗證研究[D];蘇州大學(xué);2011年

4 林苗;基于UML和時間ER網(wǎng)的嵌入式實時軟件建模與分析[D];重慶師范大學(xué);2008年

5 李偉;基于π演算的軟件體系結(jié)構(gòu)求精研究[D];湖南工業(yè)大學(xué);2008年

6 陳道喜;基于Promela的組合抽象Spin模型檢測及應(yīng)用[D];蘇州大學(xué);2009年

7 何亞麗;基于XYZ/ADL的Web服務(wù)組合驗證研究[D];蘇州大學(xué);2010年

8 張紀昌;基于場景的構(gòu)件組合方式的研究[D];浙江師范大學(xué);2010年

9 王杰;USB3.0設(shè)備控制器IP核控制端點的RTL功能驗證[D];合肥工業(yè)大學(xué);2013年

【二級參考文獻】

中國期刊全文數(shù)據(jù)庫 前8條

1 楊芙清,梅宏,呂建,金芝;淺論軟件技術(shù)發(fā)展[J];電子學(xué)報;2002年S1期

2 林惠民,張文輝;模型檢測:理論、方法與應(yīng)用[J];電子學(xué)報;2002年S1期

3 趙會群,王國仁,高遠;軟件體系結(jié)構(gòu)抽象模型[J];計算機學(xué)報;2002年07期

4 胡軍;于笑豐;張巖;王林章;李宣東;鄭國梁;;基于場景規(guī)約的構(gòu)件式系統(tǒng)設(shè)計分析與驗證[J];計算機學(xué)報;2006年04期

5 趙會群;孫晶;;面向服務(wù)的可信軟件體系結(jié)構(gòu)代數(shù)模型[J];計算機學(xué)報;2010年05期

6 文艷軍;王戟;齊治昌;;并發(fā)反應(yīng)式系統(tǒng)的組合模型檢驗與組合精化檢驗[J];軟件學(xué)報;2007年06期

7 周立;陳湘萍;黃罡;孫艷春;梅宏;;支持協(xié)商的網(wǎng)構(gòu)軟件體系結(jié)構(gòu)行為建模與驗證[J];軟件學(xué)報;2008年05期

8 劉克;單志廣;王戟;何積豐;張兆田;秦玉文;;“可信軟件基礎(chǔ)研究”重大研究計劃綜述[J];中國科學(xué)基金;2008年03期

【相似文獻】

中國期刊全文數(shù)據(jù)庫 前10條

1 李決龍;李亮;邢建春;楊啟亮;;基于交際接口的Web應(yīng)用模型檢驗[J];計算機應(yīng)用研究;2011年01期

2 楊衛(wèi)東,施伯樂;基于狀態(tài)圖的Web導(dǎo)航模型及其特性分析[J];計算機研究與發(fā)展;2002年08期

3 胡立立;繆淮扣;陳圣波;梅佳;高洪皓;;威脅驅(qū)動的Web應(yīng)用On-The-Fly導(dǎo)航模型驗證方法[J];應(yīng)用科學(xué)學(xué)報;2011年01期

4 鹿旭東;萬建成;;Web應(yīng)用開發(fā)方法研究[J];計算機工程與應(yīng)用;2006年13期

5 簡巖,秦進;一種新型高效的基于WEB應(yīng)用的校園網(wǎng)結(jié)構(gòu)模型[J];貴州師范大學(xué)學(xué)報(自然科學(xué)版);2001年03期

6 馬琳,羅鐵堅,宋進亮,葉世偉;Web性能測試與預(yù)測[J];中國科學(xué)院研究生院學(xué)報;2005年04期

7 唐海濤;王樹義;孫效里;;一種有效的Web負載均衡器的設(shè)計與實現(xiàn)[J];計算機工程;2006年20期

8 陳富節(jié);陳彪;邢詒俊;陳亞楠;廖廷悟;;淺析利用Front Controller模式構(gòu)建基于MVC模式的Web應(yīng)用[J];科技信息;2009年21期

9 金尊和 ,謝東;Domino與Web應(yīng)用 第一講 認識Domino[J];中國計算機用戶;1997年18期

10 黃學(xué)武;J2EE Web應(yīng)用性能調(diào)優(yōu)[J];計算機時代;2004年09期

中國重要會議論文全文數(shù)據(jù)庫 前10條

1 施霖;劉喻民;;層次化Web應(yīng)用模型[A];第一屆全國Web信息系統(tǒng)及其應(yīng)用會議（WISA2004）論文集[C];2004年

2 王辰龍;盧雷;;基于擴展導(dǎo)航結(jié)構(gòu)的Web應(yīng)用測試[A];第一屆全國Web信息系統(tǒng)及其應(yīng)用會議（WISA2004）論文集[C];2004年

3 師惠忠;陳波;;Web安全評估工具應(yīng)用分析[A];全國計算機安全學(xué)術(shù)交流會論文集（第二十四卷）[C];2009年

4 盧雷;萬建成;鹿旭東;郭小濤;李學(xué)慶;;基于界面組成結(jié)構(gòu)的Web界面模型[A];第一屆建立和諧人機環(huán)境聯(lián)合學(xué)術(shù)會議（HHME2005）論文集[C];2005年

5 李永堅;;主動窗體(ActiveForm)技術(shù)在Intranet中的應(yīng)用[A];廣西電機工程學(xué)會第七屆青年學(xué)術(shù)交流會論文集[C];2002年

6 李茂鑫;;小型Web應(yīng)用系統(tǒng)架構(gòu)分析與性能優(yōu)化[A];2008年計算機應(yīng)用技術(shù)交流會論文集[C];2008年

7 李驥;;煙草行業(yè)WEB應(yīng)用的威脅及防護[A];河南省煙草學(xué)會2008年學(xué)術(shù)交流獲獎?wù)撐募ㄉ希C];2008年

8 唐承華;韋皓元;;Web應(yīng)用平臺安全防護技術(shù)研究與應(yīng)急預(yù)案[A];廣西計算機學(xué)會2009年年會論文集[C];2009年

9 尹黨輝;安豐亮;董超;;談Web應(yīng)用的安全性測試技術(shù)[A];第十六屆全國青年通信學(xué)術(shù)會議論文集（上）[C];2011年

10 胡詩樵;趙文濤;趙志峰;;基于Web的可視化系統(tǒng)的設(shè)計與實現(xiàn)[A];2005通信理論與技術(shù)新進展——第十屆全國青年通信學(xué)術(shù)會議論文集[C];2005年

中國重要報紙全文數(shù)據(jù)庫 前10條

1 陳翔;FineGround優(yōu)化Web應(yīng)用[N];中國計算機報;2004年

2 合 力;捍衛(wèi)Web應(yīng)用[N];網(wǎng)絡(luò)世界;2004年

3 山楓;保護Web應(yīng)用安全[N];中國計算機報;2003年

4 王洛東編譯;XFire：揪出Web應(yīng)用中的搗蛋鬼[N];計算機世界;2004年

5 沈建苗編譯;富客戶端豐富Web應(yīng)用[N];計算機世界;2005年

6 清華大學(xué)計算機系 丁峰 徐 鵬 蔡月茹;基于Java的Web應(yīng)用概覽[N];計算機世界;2004年

7 邊 一;保護數(shù)據(jù)的Web應(yīng)用防火墻[N];網(wǎng)絡(luò)世界;2002年

8 鄭志勇;配置Web應(yīng)用環(huán)境[N];中國計算機報;2001年

9 朱新亞;Web安全評估漸熱[N];中國計算機報;2005年

10 沈文;防火墻不再“包治百病”[N];中國計算機報;2004年

中國博士學(xué)位論文全文數(shù)據(jù)庫 前7條

1 王曉鋒;Web應(yīng)用入侵異常檢測新技術(shù)研究[D];華中科技大學(xué);2007年

2 宋波;Web應(yīng)用交互的建模和測試用例生成[D];上海大學(xué);2010年

3 李雙慶;Web服務(wù)器集群技術(shù)研究[D];重慶大學(xué);2003年

4 凌海峰;基于ACO的Web使用挖掘方法研究[D];合肥工業(yè)大學(xué);2009年

5 陳俊清;可信普適服務(wù)的形式化分析與驗證[D];上海交通大學(xué);2012年

6 楊勇;SOA等級化服務(wù)替換理論與機制[D];復(fù)旦大學(xué);2011年

7 范國闖;Web應(yīng)用服務(wù)器關(guān)鍵技術(shù)研究[D];中國科學(xué)院研究生院（軟件研究所）;2004年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前10條

1 趙會朋;.NET平臺下Web系統(tǒng)構(gòu)架研究及在煤炭行業(yè)的應(yīng)用[D];西安建筑科技大學(xué);2004年

2 朱春江;基于J2EE的Web應(yīng)用研究[D];河海大學(xué);2004年

3 范潤;CORBA的Web應(yīng)用及與EJB的集成研究[D];南京理工大學(xué);2004年

4 衛(wèi)索琪;基于MVC模式的一種Web應(yīng)用框架[D];北京工業(yè)大學(xué);2003年

5 武剛;以XML為核心的WEB統(tǒng)一數(shù)據(jù)的初步研究[D];西南石油學(xué)院;2002年

6 吳少華;Web應(yīng)用的細粒度訪問控制技術(shù)研究[D];四川大學(xué);2003年

7 李玉強;基于COM技術(shù)與JNI技術(shù)的通用數(shù)據(jù)交換技術(shù)的研究[D];武漢理工大學(xué);2005年

8 周中雨;WEB應(yīng)用監(jiān)測系統(tǒng)的研究與實現(xiàn)[D];清華大學(xué);2004年

9 符寧;Web應(yīng)用程序開發(fā)技術(shù)及工具的研究[D];西北工業(yè)大學(xué);2005年

10 張芳;面向電子商務(wù)的Web應(yīng)用元模型的研究與實現(xiàn)[D];國防科學(xué)技術(shù)大學(xué);2004年

，

本文編號：707974