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

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

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

【參考文獻(xiàn)】

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

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

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

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

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

【共引文獻(xiàn)】

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

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

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

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

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

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

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

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

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

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

10 丁佐華;江明月;劉靜;;基于常微分方程的死鎖檢測(cè)實(shí)驗(yàn)分析[J];計(jì)算機(jī)學(xué)報(bào);2009年09期

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

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

2 曾紅衛(wèi);Web應(yīng)用的驗(yàn)證與測(cè)試方法研究[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 劉智;二進(jìn)制代碼級(jí)的漏洞攻擊檢測(cè)研究[D];電子科技大學(xué);2013年

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

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

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

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

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

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

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

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

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

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

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

【二級(jí)參考文獻(xiàn)】

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

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

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

3 趙會(huì)群,王國(guó)仁,高遠(yuǎn);軟件體系結(jié)構(gòu)抽象模型[J];計(jì)算機(jī)學(xué)報(bào);2002年07期

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

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

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

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

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

【相似文獻(xiàn)】

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

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

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

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

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

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

6 馬琳,羅鐵堅(jiān),宋進(jìn)亮,葉世偉;Web性能測(cè)試與預(yù)測(cè)[J];中國(guó)科學(xué)院研究生院學(xué)報(bào);2005年04期

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

中國(guó)重要報(bào)紙全文數(shù)據(jù)庫(kù) 前10條

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

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

3 山楓;保護(hù)Web應(yīng)用安全[N];中國(guó)計(jì)算機(jī)報(bào);2003年

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

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

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

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

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

9 朱新亞;Web安全評(píng)估漸熱[N];中國(guó)計(jì)算機(jī)報(bào);2005年

10 沈文;防火墻不再“包治百病”[N];中國(guó)計(jì)算機(jī)報(bào);2004年

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

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

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

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

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

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

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

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

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

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

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

3 范潤(rùn);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)用的細(xì)粒度訪問控制技術(shù)研究[D];四川大學(xué);2003年

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

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

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

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

，

本文編號(hào)：707974