INTRODUCTION

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 specification 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 specifications are mostly used in critical systems where the cost of failure is catastrophic. Formal specifications can be used in several ways of design cycle, static verification and test generation being the most notable. applications. Then abstract test cases were generated from the State chart model in our ACT tool. Abstract test cases cannot be directly executed on the implementation since they are defined using elements and objects of the State chart model, and must be first transformed to concrete test cases. So finally, concrete executable Selenium RC JUnit test cases are generated from these abstract test cases in our ACT tool which can be directly executed on the implementation. The remainder of the paper is organized as follows. Section 2 gives a brief review of related work, while Section 3 explains the proposed methodology used by our ACT tool. Section 4 illustrates the State chart specification for modeling the navigation behaviour of web applications. Section 5 illustrates the generation of test path from the State chart model. Section 6 illustrates how abstract test cases are generated using Symbolic execution and SMT solver. Section 7 illustrates the translation of abstract test cases to concrete test cases. Section 8 concludes the paper and Section 9 gives scope for future work.

RELATED WORK

A number of formal, informal and semi-formal models like automata [2], Statechart [3], UML and OCL [ 5], UML based web engineering, alloy, directed graph and control flow graphs, SDL, term rewriting systems, XML have been proposed in various studies [6] for modeling web applications. The authors in [5] have proposed UML class diagram and the authors in [3] have proposed statechart for modeling web navigation. A methodology for generation of concrete executable tests from abstract test cases using a test automation language, the Structured Test Automation Language (STAL) was proposed in [7]. The authors in [7] have proposed a mapping between identifiable elements in the model to JUnit executable java code. The author in [8] have presented an approach using domain specific languages to model the navigation aspect of the web application and have used a UI mapping XML file to generate concrete test cases for Selenium and Canoo web test tools. In [8], an approach that utilizes recorded user interaction data to construct a state machine model especially for testing AJAX functionality is presented. Input data is provided from the collected requests and test oracles have to be created manually. The generated test sequences are translated into the test case format of the Selenium test automation tool. The authors in [9] have used model checking to generate test cases for control flow and data flow coverage criteria. The authors in [10] 2nd Modelling Symposium (ModSym 2016) -colocated with ISEC 2016, Goa, India, Feb 18, 2016

PROPOSED METHODOLOGY

A FORMAL MODEL FOR WEB NAVI-GATION -STATE CHART

From among the various finite state based formal specification languages, we have used Statecharts [1] for modeling the navigation behaviour of web applications. Figure 2 shows the State chart specification of our case study, the Learning Management System (LMS) used within our institute.

In the Statechart specification shown in Figure 2

TEST PATH GENERATION FROM STATE CHART MODEL

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 verification technique can also be used to generate test paths by formulating a temporal logic specification as a trap property to be verified. The straight forward way to represent a State chart as a transition system is to flatten its hierarchy. In our approach, the hierarchical State chart navigation model was first flattened and then transformed into an SMV program. The trap properties for navigation were written in CTL formulas and then the Symbolic Model Verifier (NuSMV) tool is executed which generates the counter examples. For example, the CTL Trap Specification Property for specifying that state SE-230 Software Testing is reachable from the initial state is:

CTL Trap Specification 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.

Add.clicked/ / [!username1!∈! valid_student_usernames!!∧! password1!∈! valid_student_passwords!]! Add.clicked/ / [!username1!∈!! valid_teacher_usernames/∧! password1!∈! valid_teacher_passwords!]! Add.clicked/ [!username1!∉ !"#$%_!"#$ℎ!"_!"#$%&'#"!∧! password1!∉ !"#$%_!"#$ℎ!"_!"##$%&'#!]!/! ! valid_teacher_usernames/:=/valid_teacher_usernames/// ∪ !"#$%&'#!! ∧/ valid_teacher_passwords/:=/valid_teacher_passwords/ ∪/password! Login.clicked/ [!username2!∈!valid_student_usernames!!∧! password2!∈!valid_student_passwords!!]! ! ! Login.clicked/ [!username!=!valid_admin_username!/∧!/ !!!!password!=!valid_admin_password!]! Login.clicked/ [!username3!∈!!valid_teacher_usernames!/∧/ !!!password3!!∈!!valid_teacher_passwords!]! ! CSISEI270!(username1 = "") ∧ (password1 = "") ∧ (username1 / ∈ φ) ∧ (password1 / ∈ φ).

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 = ""∧(password1 = "")∧(username1 / ∈ φ)∧(password1 / ∈ φ)∧(username2 ∈ username1)∧(password2 ∈ password1)) So the final path predicate for the counter example ! EF(state=SE-230 Software Testing ) is: ((username1 = "" ∧ (password1 = "") ∧ (username1

/ ∈ φ) ∧ (password1 / ∈ φ) ∧ (username2 ∈ username1)∧ (password2 ∈ 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 [11] would determine if the path predicate is satisfiable, and if yes, then it will generate satisfying values for the symbolic variables occurring in the formula and hence the concrete input values would be generated. Suppose, if a counter example is generated for the path from state Inactive to state Error Page through states LMS Login, Admin Home Page, Add Users and Add Student User Page, then the path predicate formed will be: (username1 ∈ φ) ∧ (password1 ∈ φ) which will be a contradiction i.e. unsatisfiable predicate. Hence, this path will be rejected as infeasible. still abstract because firstly variables like username1, pass-word1, 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 specification and are only available after the exact implementation is finished. 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 specification 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 file 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 file is created manually. Since, the State chart model contained only partial information of the final implementation. So, now the additional information that were abstracted out from the State chart model has to be added in the Mappings XML file 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 fields like Name and Department which were abstracted out in the State chart specification of Figure 2. So these fields were also included in the Mappings XML file. Using the generated abstract test cases from the previous step and the mappings XML file 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.

Abstract Test Cases Generation

TRANSLATION OF ABSTRACT TEST CASES TO CONCRETE TEST CASES

RESULTS

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. 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.

CONCLUSION

Test cases generated from formal specifications 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 flow 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-flow between atomic interaction. The resulting abstract test cases are concrete enough so that the mapping method is effective 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 file, 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 specification.