中文

Journal of Applied Sciences ›› 2011, Vol. 29 ›› Issue (1): 83-92.doi: 10.3969/j.issn.0255-8297.2011.01.015

• Computer Science and Applications • Previous Articles     Next Articles

Threat-Driven On-The-Fly Verification of Navigation Model for Web Applications

HU Li-li1;2, MIAO Huai-kou1;2, CHEN Sheng-bo1;2, MEI Jia1, GAO Hong-hao1   

  1. 1. School of Computer Engineering and Science, Shanghai University, Shanghai 200072, China
    2. Shanghai Key Laboratory of Computer Software Testing and Evaluating, Shanghai 201112, China
  • Received:2010-10-15 Revised:2010-11-08 Online:2011-01-26 Published:2011-01-25

PDF

1927

Cited

1

Abstract:

Security of network software such as Web applications has drawn much attention in the industry.Modeling and verifying Web applications involving intricate interactions are a challenge to software developers.In this paper, we propose a threaten-driven approach to model and verify the on-the-fly navigation model of Web applications. Security properties are extracted from the model based on the threaten-driven method. Using the model checking tool NuSMV, we have verified the model. The experimental results indicate that the proposed approach can avoid state space explosion to a certain extent.

Key words: on-the-fly verification, Web application, security property

CLC Number: