TY - GEN
T1 - Symbolic verification of web crawler functionality and its properties
AU - Shetty, Keerthi S.
AU - Bhat, Swaraj
AU - Singh, Sanjay
PY - 2012/3/27
Y1 - 2012/3/27
N2 - Now a days people use search engines every now and then to retrieve documents from the Web. Web crawling is the process by which a search engine gather pages from the Web to index them and support a search engine. Web crawlers are the heart of search engines. Web crawlers continuously keep on crawling the web and find any new web pages that have been added to the web, pages that have been removed from the web. Due to growing and dynamic nature of the web, it has become a challenge to traverse through all URLs in the web documents and to handle these URLs. The entire crawling process may be viewed as traversing a web graph. The aim of this paper is to model check the crawling process and crawler properties using a symbolic model checker tool called NuSMV. The basic operation of a hypertext crawler and the crawler properties has been modeled in terms of CTL specification and it is observed that the system takes care of all the constraints by satisfying all the specifications.
AB - Now a days people use search engines every now and then to retrieve documents from the Web. Web crawling is the process by which a search engine gather pages from the Web to index them and support a search engine. Web crawlers are the heart of search engines. Web crawlers continuously keep on crawling the web and find any new web pages that have been added to the web, pages that have been removed from the web. Due to growing and dynamic nature of the web, it has become a challenge to traverse through all URLs in the web documents and to handle these URLs. The entire crawling process may be viewed as traversing a web graph. The aim of this paper is to model check the crawling process and crawler properties using a symbolic model checker tool called NuSMV. The basic operation of a hypertext crawler and the crawler properties has been modeled in terms of CTL specification and it is observed that the system takes care of all the constraints by satisfying all the specifications.
UR - https://www.scopus.com/pages/publications/84863343721
UR - https://www.scopus.com/inward/citedby.url?scp=84863343721&partnerID=8YFLogxK
U2 - 10.1109/ICCCI.2012.6158649
DO - 10.1109/ICCCI.2012.6158649
M3 - Conference contribution
AN - SCOPUS:84863343721
SN - 9781457715822
T3 - 2012 International Conference on Computer Communication and Informatics, ICCCI 2012
BT - 2012 International Conference on Computer Communication and Informatics, ICCCI 2012
T2 - 2012 International Conference on Computer Communication and Informatics, ICCCI 2012
Y2 - 10 January 2012 through 12 January 2012
ER -