کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
551681 873072 2013 18 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
A formal approach for run-time verification of web applications using scope-extended LTL
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر تعامل انسان و کامپیوتر
پیش نمایش صفحه اول مقاله
A formal approach for run-time verification of web applications using scope-extended LTL
چکیده انگلیسی

ContextIn the past decade, the World Wide Web has been subject to rapid changes. Web sites have evolved from static information pages to dynamic and service-oriented applications that are used for a broad range of activities on a daily basis. For this reason, thorough analysis and verification of Web Applications help assure the deployment of high quality applications.ObjectivesIn this paper, an approach is presented to the formal verification and validation of existing web applications. The approach consists of using execution traces of a web application to automatically generate a communicating automata model. The obtained model is used to model checking the application against predefined properties, to perform regression testing, and for documentation.MethodsTraces used in the proposed approach are collected by monitoring a web application while it is explored by a user or a program. An automata-based model is derived from the collected traces by mapping the pages of the application under test into states and the links and forms used to browse the application into transitions between the states. Properties, meanwhile, express correctness and quality requirements on web applications and might concern all states of the model; in many cases, these properties concern only a proper subset of the states, in which case the model is refined to designate the subset of the global states of interest. A related problem of property specification in Linear Temporal Logic (LTL) over only a subset of states of a system is solved by means of specialized operators that facilitate specifying properties over propositional scopes in a concise and intuitive way. Each scope constitutes a subset of states that satisfy a propositional logic formula.ResultsAn implementation of the verification approach that uses the model checker Spin is presented where an integrated toolset is developed and empirical results are shown. Also, Linear Temporal Logic is extended with propositional scopes.Conclusiona formal approach is developed to build a finite automata model tuned to features of web applications that have to be validated, while delegating the task of property verification to an existing model checker. Also, the problem of property specification in LTL over a subset of the states of a given system is addressed, and a generic and practical solution is proposed which does not require any changes in the system model by defining specialized operators in LTL using scopes.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information and Software Technology - Volume 55, Issue 12, December 2013, Pages 2191–2208
نویسندگان
, , , ,