Modeling, Verification and Testing of Web Applications Using Model Checker
スポンサーリンク
概要
- 論文の詳細を見る
The number of Web applications handling online transaction is increasing, but verification of the correctness of Web application development has been done manually. This paper proposes a method for modeling, verifying and testing Web applications. In our method, a Web application is modeled using two finite-state automata, i.e., a page automaton which specifies Web page transitions, and an internal state automaton which specifies internal state transitions of the Web application. General properties for checking the Web application design are presented in LTL formulae and they are verified using the model checker Spin. Test cases examining the behavior of the Web application are also generated by utilizing the counterexamples obtained as the result of model checking. We applied our method to an example Web application to confirm its effectiveness.
- （社）電子情報通信学会の論文
- 2011-05-01
著者
-
TAKAHASHI Kaoru
Sendai National College of Technology
-
Togashi Atsushi
Graduate School Of Project Design Miyagi University
-
HOMMA Kei
Graduate School of Project Design, Miyagi University
-
IZUMI Satoru
Research Institute of Electrical Communication/Graduate School of Information Sciences, Tohoku Unive
-
Izumi Satoru
Research Institute Of Electrical Communication/graduate School Of Information Sciences Tohoku Univer
-
Homma Kei
Graduate School Of Project Design Miyagi University
-
Izumi Satoru
Research Institute of Electrical Communication Tohoku University
関連論文
- Composition of Service and Protocol Specifications in Asynchronous Communication System(Networks)
- State Machine Specification with Reusability(Concurrent Systems)(Concurrent Systems and Hybrid Systems)
- Specification and Analysis of the Contract Net Protocol Based on State Machine Model(Special Section on Concurrent System Technology and Its Application to Multiple Agent Systems)
- On Constructing n-Entities Communication Protocol and Service with Alternative and Concurrent Functions(Special Section on Concurrent System Technology and Its Application to Multiple Agent Systems)
- Specification of a Concurrent System Based on Propositional Logic (特集:マルチメディア通信と分散処理)
- Composition of Protocol Functions(Special Section on Concurrent Systems Technology)
- Specification and Validation of a Dynamically Reconfigurable System(Special Section on Concurrent Systems Technology)
- A Concurrent Calculus with Geographical Constraints(Special Section on Concurrent Systems Technology)
- Making Changes in Formal Protocol Specifications
- A Topological Framework of Stepwise Specification for Concurrent Systems (Special Section on Description Models for Concurrent Systems and Their Applications)
- On Specifying Protocols Based on LOTOS and Temporal Logic
- A Consideration Of Integrated System Management In OSI Environment
- An Improvement of The Protocol Synthesis Algorithm
- A Compositional Approach for Constructing Communication Services and Protocols (Special Section on Concurrent Systems Technology)
- An Error Detection Method for Recursive Processes for LOTOS Instruction and Its Support System
- A Flexible Verifier of Temporal Properties for LOTOS
- Modeling, Verification and Testing of Web Applications Using Model Checker
- BS-1-36 G/D-MIB:A Proposal of Green-oriented Disaster-resistant Management Information Base