Verification of Web application based on CEGAR approach

被引：0
|
作者：
Gao, Hong-Hao [1 ,2 ,3 ]
Miao, Huai-Kou [1 ,3 ]
Zeng, Hong-Wei [1 ]
机构：
[1] School of Computer Engineering and Science, Shanghai University
[2] Computing Center, Shanghai University
[3] Shanghai Key Laboratory of Computer Software Evaluating and Testing
来源：
Gao, H.-H. (gaohonghao@shu.edu.cn) | 1600年 / Science Press卷 / 37期
关键词：
Abstraction refinement; Model checking; Navigation model; Spurious counterexample; Web application;
D O I：
10.3724/SP.J.1016.2014.00976
中图分类号：
学科分类号：
摘要：
How to model and verify navigational behaviors of Web application is the key issue to ensure the reliability of Web engineering. After analyzing the interactive behaviors between the user and Web browser, this paper applies On-the-fly strategy and Counterexample-Guided Abstraction Refinement (CEGAR) method to Web application modeling, abstraction refinement and verification. When the navigation model is constructed on the fly, a verification property based incremental state abstraction approach is proposed to generate the corresponding abstract navigation model. Then, an equivalence classes-based abstraction refinement is introduced to eliminate the spurious counterexample if the abstract counterexample is proven to be false. In conclusion, our approach can effectively alleviate the state explosion problem of Web application verification.
引用
收藏
页码：976 / 992
页数：16
相关论文
共 40 条
  • [1] Clarke E.M., Grumberg O., Peled D.A., Model Checking, (2000)
  • [2] Haydar M., Petrenko A., Sahraoui H., Formal verification of Web Applications modeled by communicating automata, Proceedings of the 24th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2004), pp. 115-132, (2004)
  • [3] Donini F.M., Mongiello M., Ruta M., Totaro R., A model checking-based method for verifying Web application design, Electronic Notes in Theoretical Computer Science, 151, 2, pp. 19-32, (2006)
  • [4] Han M., Hofmeister C., Modeling and verification of adaptive navigation in Web applications, Proceedings of the 6th International Conference on Web Engineering (ICWE 2006), pp. 329-336, (2006)
  • [5] Courcoubetis C., Vardi M., Wolper P., Yannakakis M., Memory efficient algorithms for the verification of temporal properties, Proceedings of the 2nd International Workshop on Computer Aided Verification (CAV 1990), pp. 233-242, (1990)
  • [6] Wen Y.-J., Wang J., Qi Z.-C., Compositional model checking and compositional refinement checking of concurrent reactive systems, Journal of Software, 18, 6, pp. 1270-1281, (2007)
  • [7] Bryant R.E., Symbolic Boolean manipulation with ordered binary decision diagrams, ACM Computing Surveys, 24, 3, pp. 293-318, (1992)
  • [8] Alur R., Brayton R.K., Henzinger T.A., Et al., Partial-order reduction in symbolic state space exploration, Proceedings of the 9th International Conference on Computer Aided Verification (CAV 1997), pp. 340-351, (1997)
  • [9] Berezin S., Campos S.V., Clarke E.M., Compositional reasoning in model checking, Proceedings of the Revised Lectures From the international Symposium on Compositionality: The Significant Difference (COMPOS 1997), pp. 81-102, (1997)
  • [10] Henzinger T.A., Qadeer S., Rajamani S.K., Tasiran S., An assume-guarantee rule for checking simulation, ACM Transactions on Programming Languages and Systems, 24, 1, pp. 51-64, (2002)
1234