Paper Info
Title
A formal approach for run-time verification of web applications using scope-extended LTL
Abstract
Context: In 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. Objectives: In 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. Methods: Traces 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. Results: An 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. Conclusion: a 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.
Year
DOI
Venue
2013
10.1016/j.infsof.2013.07.013
Information & Software Technology
Keywords
Field
DocType
automata model,existing model checker,finite automata model,formal approach,property specification,linear temporal logic,specialized operator,scope-extended ltl,web application,automata-based model,run-time verification,propositional scope,model checker spin,dynamic analysis,web applications,model checking,web engineering
Computation tree logic,Data mining,Programming language,Model checking,Computer science,Correctness,Web engineering,Theoretical computer science,Linear temporal logic,Web modeling,Web application,Formal verification
Journal
Volume
Issue
ISSN
55
12
0950-5849
Citations 
PageRank 
References 
5
0.43
28
Authors
4
Name
Order
Citations
PageRank
May Haydar1593.05
A. Petrenko256531.37
Sergiy Boroday329414.03
Houari Sahraoui480142.47