As web applications are becoming more and more ubiquitous, modeling and testing web applications correctly is becoming necessary. In this paper, we have used a formal speci cation language, State chart to model the navigation behaviour aspect of web applications. This paper presents the ACT (Abstract to Concrete Tests) tool, an approach of generating concrete executable Selenium RC JUnit test cases from a formal State chart speci cation model. The ACT tool can generate concrete Selenium RC JUnit test cases from abstract test cases by utilizing data shared across di erent interactions of the web application with the web server. Throughout the paper, a case study of Learning Management System is used to illustrate our approach.
Nowdays, the use of web applications has grown to a huge extent. Web applications are used in online shopping, online banking, etc., so designing and testing web applications rigorously has become very crucial. Formal speci cation languages are used to clarify customer's requirements by removing ambiguity, inconsistency and incompleteness in the software requirements and design process. Thus, they are helpful in reducing the requirement errors in the early stages of the software development life cycle. Formal speci cations are mostly used in critical systems where the cost of failure is catastrophic. Formal speci cations can be used in several ways of design cycle, static veri cation and test generation being the most notable.
In this paper, we present the ACT (Abstract to Concrete
Tests) tool, which uses a novel approach of generating
concrete test cases from abstract test cases by using data shared
across di erent interactions of the web application with the
web server. A formal speci cation language `Statecharts' [
A number of formal, informal and semi-formal models like
automata [
From among the various nite state based formal speci
cation languages, we have used Statecharts [
The front end step in the ACT tool which generates test paths can be any test path generating algorithm like graph coverage algorithms. But model checking which is a formal veri cation technique can also be used to generate test paths by formulating a temporal logic speci cation as a trap property to be veri ed. The straight forward way to represent a State chart as a transition system is to atten its hierarchy. In our approach, the hierarchical State chart navigation model was rst attened and then transformed into an SMV program. The trap properties for navigation were written in CTL formulas and then the Symbolic Model Veri er (NuSMV) tool is executed which generates the counter examples. For example, the CTL Trap Speci cation Property for specifying that state SE-230 Software Testing is reachable from the initial state is: CTL Trap Speci cation Property: ! EF(state=SE-230 Software Testing) This trap property will generate a counter example which is our test path. For this counter example there will be two paths. One from LMS Login Page to My Courses Page to SE-230 Software Testing Page. And the second test path will be the loop from LMS Login Page to Successfully Student Added Page then to My Course Page to SE-230 Software Testing page. Here we will restrict the length of the loop in the counter example by using bounded model checking and set the length of the counter example to a xed size. The CTL Trap properties for generating test paths are written for various requirements of the web application, like the top page of a web application should be reachable from all the pages of the web application. In addition, we also wrote CTL trap properties for node coverage criterion.
Login.clicked/ [!username2!∉!valid_student_usernames/⋁!!! !!password2!!∉!valid_student_passwords!!!]!
Login.clicked/ [!username!∉!valid_teacher_usernames/⋁!!! !!password!!∉!valid_teacher_passwords!!!]! !
Login.clicked/ [!username2!∈!valid_student_usernames!!∧! password2!∈!valid_student_passwords!!]! !
My!Courses!! Design/and/Analysis/ of/ Safety/Critical/ Systems.clicked/
Login.clicked/ [!username3!∈!!valid_teacher_usernames!/∧/ !!!password3!!∈!!valid_teacher_p a!sswords!]! ! Software/ Testing.clicked/ CSISEI270!Design_and_Analysis!! _Of_SafetyICritical_Systems! SEI230_Software! _Testing! Grades.clicked/
News/
Forum.clicked/ Grades!Page!
General/ Discussion/
Forum.clicked/ News!Forum!
General!Discussion! !
Forum!
Slides/ Folder.clicked/ Slides!Folder! page!
LMS!Login!Page! !
Logout.clicked/ My!Courses! TDD/ Assignment.clicked/
Test!Driven!! Developemnt! Assignment!Page!
Login.clicked/ [!username!=!valid_admin_username!/∧!/ !!!!password!=!valid_admin_password!]!
Logout.clicked/ Admin!Home!!
Page! Add!Users!
Add.clicked/ [!username1!∉!valid_student_usernames!∧! password1!∉!valid_student_passwords!]!/! ! valid_student_usernames/:=/ valid_student_usernames/∪/username///∧/ valid_student_passwords/:=/ valid_student_passwords/∪/password//
Successfully! Student!Added!
Page!
After the test paths are generated from the State chart model, symbolic execution is carried out to generate input values to guide the execution along the test paths. The path predicate corresponding to the test path is computed. This, in turn, is given to an SMT solver to generate concrete input values. These values are used to generate the abstract test cases. The algorithm used to generate the abstract test cases using symbolic execution is shown in the block diagram in Figure 3. 6.1
This section illustrates the method of formation of path predicates and the generation of concrete values using the example of the counter example generated from the CTL Trap Property !EF(state=SE-230 Software Testing). The variables valid student usernames and valid student passwords in the State chart model in Figure 2 are internal program variables and are internally maintained as sets. These variables are initialized to null in the transition from state Inactive to composite state Active as shown in Figure 2. The path predicate formed for the transition from Add Student User Page to Successfully Student Added Page is (username1 6= "") ^ (password1 6= "") ^ (username1 2= ) ^ (password1 2= ).
Sets valid student usernames and valid student passwords are
consequently updated to username1 and password1. So the
path predicate for the transition from state LMS Login Page
to My Courses is ((username1
6= ""^(password1 6= "")^(username1 2= )^(password1 2=
)^(username2 2 username1)^(password2 2 password1))
So the nal path predicate for the counter example
! EF(state=SE-230 Software Testing ) is: ((username1 6=
"" ^ (password1 6= "") ^ (username1 2= ) ^ (password1 2=
) ^ (username2 2 username1)^
(password2 2 password1))
Here username1 and password1 are the symbolic variables
corresponding to the Add Student User page, and username2
and password2 are the symbolic variables corresponding to
the LMS Login page. An SMT solver like CVC3 [
Symbolic
Execution
Path Predicate Extraction Form Test
Case
Concrete Values
SMT Solver
The last step is deriving concrete executable test cases from these abstract test cases so these concrete test cases can communicate directly with the system under test. The abstract test cases generated from the State chart model are on the same level of abstraction as the model since the State chart model they are generated from contains only partial information of the implementation under test. In Figure 5, even through the input values are concrete, the test case is username=\admin" password=\admin" Login.clicked Add Users.clicked Add Student.clicked username1=\MS2013009" password1=\abc" Add.clicked Logout.clicked username2=\MS2013009" password2=\abc" Login.clicked Software Testing.clicked still abstract because rstly variables like username1, password1, etc. needs to be mapped to the implementation entities . And, secondly many of the inputs that may be needed may not be there in the original speci cation and are only available after the exact implementation is nished. For generating concrete test cases from the abstract test cases generated in the previous step, the ACT tool uses a mapping between phrases used in the State chart speci cation model to Selenium Remote Control JUnit test code which helps to translate an abstract test to concrete Selenium RC JUnit test. Figure 8 shows a part of XML le that was created to give a mapping between the phrases in the State chart model of Figure 2 to Selenium RC JUnit java code for our case study of Learning Management System. The mappings XML le is created manually. Since, the State chart model contained only partial information of the nal implementation. So, now the additional information that were abstracted out from the State chart model has to be added in the Mappings XML le in order to generate the concrete Selenium RC Junit test cases. From the source code implementation of the case study of HMS, we found that in the Add Student User page there were additional input elds like Name and Department which were abstracted out in the State chart speci cation of Figure 2. So these elds were also included in the Mappings XML le. Using the generated abstract test cases from the previous step and the mappings XML le created manually and fed as input to the ACT tool, a set of concrete Selenium RC Junit test cases is generated in this step. Figure 5 shows one of the concrete Selenium JUnit test case generated from our ACT tool for the case study of Learning Management System.
For two other web based enterprise applications developed within our institute, a Hospital Management System (HMS) and a Student Information System (SIS), we modeled our web applications using the proposed method.
Table 2 shows the lines of code (LOC) of the two systems, the number of nodes in the attened State chart (Nflat), the number of mappings and the number of abstract test cases( or counter examples) used for the various test coverage criterion. A total of 14 abstract test cases were used for HMS <mappings> <mapping> <phrase>state</phrase> <value>Add Student User</value> <code> selenium=new DefaultSelenium(\localhost",4444," refox/" +\Applications/Fire+\ refoxfox.app/Contents/MacOS/" bin",\https://lms.iiitb.ac.in/moodle");" selenium.start(); selenium.open(\/course/view.php?id=19"); </code> </mapping> <mapping> <phrase>username1</phrase> <value>u1</value> <range>non blank</range> <code>selenium.type (\css=input[id='username',]",u1);</code> </mapping> <mapping> <phrase>Name</phrase> <value>n</value> <code> selenium.type(\css=input[id='name']",n); </code> </mapping> <mapping> <phrase>Department</phrase> <value>dp</value> <code> selenium.type(\css=input[id='department']",dp);</code> </mapping> </mappings> system and a total of 53 abstract test cases were used for SIS System for various test criterion. Currently, we have modelled the two case studies of HMS System and SIS System but we are currently running our ACT tool and trying to calculate the number of concrete test cases that would be generated. 9.
Test cases generated from formal speci cations are often at an abstract level. They cannot be executed directly using a test automation tool, e.g. Selenium. The existing methods have tried to deal with this problem using a mapping approach. However, this approach is fundamentally limited in its capability to translate abstract test cases into concrete test case due to the presence of data ow relationship between atomic interactions between the (test-)client and the server. In this paper, we have presented a precise characterisation of this problem. Further, we have provided a test generation methodology which uses symbolic execution to resolve the data- ow between atomic interaction. The resulting abstract test cases are concrete enough so that the mapping method is e ective in completely translating them to concrete test cases that can be directly executed on Selenium test runner. Through some of the steps like creation of Mappings XML le, construction of State chart, etc are manual but there is fairly a reasonable automation in the other steps in the ACT tool. Therefore, our approach is able to achieve a reasonable amount of end to end automation of the test generation process from formal speci cation.
Web Applications 133 15,770 20 56 10. FUTURE WORK In our future work, we will try to address the following issues:
Currently we are running our ACT tool on our LMS system and we are currently trying to nd out the number of concrete test cases that would be generated for various test criteria. So in our future work, we will try to nd out the relation between the number of concrete test cases and the number of abstract test cases and we will also try to see how the number of concrete test case and the number of abstract test cases varies with the size of the State chart model.
In our future work, we will generalise this approach to apply other forms of formal speci cation and coverage criteria. In addition, we intend to apply other forms of front-end techniques like graph coverage criteria in generating test paths instead of the model checking approach for generation of test paths . 11. selenium . start (); selenium . open (" ROOT / login / index . php "); selenium . type (" css = input [id=' username ']", " admin "); selenium . type (" css = input [id=' password ']", " admin "); selenium . click (" xpath =// a[ contains (@href , 'ROOT / myadmin / ')]"); selenium . click (" xpath =// a[ contains (@href , 'ROOT / user / index . php ?id =27 ')] "); selenium . click (" xpath =// a[ contains (@href , 'ROOT ' selenium . type (" css = input [id=' username1 ']", " Joe "); selenium . type (" css = input [id=' password1 ']", " abc "); selenium . click ("// input [ @id =' loginbtn ']"); selenium . click (" xpath =// a[ contains (@href , 'ROOT / login / index . php ')]"); selenium . type (" css = input [id=' username2 ']", " Joe "); selenium . type (" css = input [id=' password2 ']", " abc "); selenium . click (" xpath =// a[ contains (@href , 'ROOT /my / ')]"); selenium . click (" xpath =// a[ contains (@href , 'ROOT / course / view . php ?id =19 ')] ");