Properties and scopes in web model checking

We consider a formal framework for property verification of web applications using Spin model checker. Some of the web related properties concern all states of the model, while others – only a proper subset of them. To be able to discriminate states of interest in the state space, we solve the problem of property specification in LTL over a subset of states of a system under test while ignoring the valuation of the properties in the rest of them. We introduce specialized operators that facilitate specifying properties over propositional scopes, where each scope constitutes a subset of states that satisfy a propositional logic formula. Using the proposed operators, the user can specify web properties more concisely and intuitively. We illustrate the proposed solution in specifying properties of web applications and discuss other potential applications. Categories and Subject Descriptors D.2.4 [Software/Program Verification]: Formal methods, Model checking, Validation; F.4 [Mathematic...

• Type: Conference
• Year: 2005
• Where: KBSE
• Authors: May Haydar, Sergiy Boroday, Alexandre Petrenko, Houari A. Sahraoui
• Keywords: KBSE 2005, Software Engineering, Temporal Logic, Web Applications, Web Related Properties