=Paper=
{{Paper
|id=Vol-1561/paper3
|storemode=property
|title=ACT (Abstract to Concrete Tests) - A Tool for Generating Concrete Test Cases from Formal Specification of Web Applications
|pdfUrl=https://ceur-ws.org/Vol-1561/paper3.pdf
|volume=Vol-1561
|dblpUrl=https://dblp.org/rec/conf/indiaSE/BubnaC16
}}
==ACT (Abstract to Concrete Tests) - A Tool for Generating Concrete Test Cases from Formal Specification of Web Applications==
https://ceur-ws.org/Vol-1561/paper3.pdf
ACT (Abstract to Concrete Tests) - A tool for generating
Concrete test cases from Formal Specification of Web
Applications
Khusbu Bubna Sujit Kumar Chakrabarti
International Institute of Information Technology, International Institute of Information Technology,
Bangalore Bangalore
khusbu.bubna@iiitb.org sujitkc@iiitb.ac.in
ABSTRACT applications. Then abstract test cases were generated from
As web applications are becoming more and more ubiqui- the State chart model in our ACT tool. Abstract test cases
tous, modeling and testing web applications correctly is be- cannot be directly executed on the implementation since
coming necessary. In this paper, we have used a formal they are defined using elements and objects of the State
specification language, State chart to model the navigation chart model, and must be first transformed to concrete test
behaviour aspect of web applications. This paper presents cases. So finally, concrete executable Selenium RC JUnit
the ACT (Abstract to Concrete Tests) tool, an approach test cases are generated from these abstract test cases in our
of generating concrete executable Selenium RC JUnit test ACT tool which can be directly executed on the implemen-
cases from a formal State chart specification model. The tation. The remainder of the paper is organized as follows.
ACT tool can generate concrete Selenium RC JUnit test Section 2 gives a brief review of related work, while Section
cases from abstract test cases by utilizing data shared across 3 explains the proposed methodology used by our ACT tool.
different interactions of the web application with the web Section 4 illustrates the State chart specification for model-
server. Throughout the paper, a case study of Learning ing the navigation behaviour of web applications. Section 5
Management System is used to illustrate our approach. illustrates the generation of test path from the State chart
model. Section 6 illustrates how abstract test cases are gen-
erated using Symbolic execution and SMT solver. Section 7
1. INTRODUCTION illustrates the translation of abstract test cases to concrete
Nowdays, the use of web applications has grown to a huge test cases. Section 8 concludes the paper and Section 9 gives
extent. Web applications are used in online shopping, online scope for future work.
banking, etc., so designing and testing web applications rig-
orously has become very crucial. Formal specification lan- 2. RELATED WORK
guages are used to clarify customer’s requirements by re-
moving ambiguity, inconsistency and incompleteness in the A number of formal, informal and semi-formal models like
software requirements and design process. Thus, they are automata [2], Statechart [3], UML and OCL [ 5], UML
helpful in reducing the requirement errors in the early stages based web engineering, alloy, directed graph and control flow
of the software development life cycle. Formal specifications graphs, SDL, term rewriting systems, XML have been pro-
are mostly used in critical systems where the cost of failure posed in various studies [6] for modeling web applications.
is catastrophic. Formal specifications can be used in several The authors in [5] have proposed UML class diagram and
ways of design cycle, static verification and test generation the authors in [3] have proposed statechart for modeling web
being the most notable. navigation. A methodology for generation of concrete exe-
cutable tests from abstract test cases using a test automa-
In this paper, we present the ACT (Abstract to Concrete tion language, the Structured Test Automation Language
Tests) tool, which uses a novel approach of generating con- (STAL) was proposed in [7]. The authors in [7] have pro-
crete test cases from abstract test cases by using data shared posed a mapping between identifiable elements in the model
across different interactions of the web application with the to JUnit executable java code. The author in [8] have pre-
web server. A formal specification language ‘Statecharts’ [1] sented an approach using domain specific languages to model
was used to model the navigation behaviour aspect of web 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
Copyright c 2016 for the individual papers by the papers’ authors. Copy- Selenium test automation tool. The authors in [9] have used
ing permitted for private and academic purposes. This volume is published
and copyrighted by its editors. 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
16
name and password. Thus there is a data flow between Add
Student User Page page and LMS Login Page. The vari-
ables valid student usernames and valid student passwords
are defined in the transition from state Add Student User
Page to Successfully Student Added Page and are used in
the transition from state LMS Login Page to My Courses
web page. The variables valid student usernames,
valid student passwords, valid teacher usernames and
valid teacher passwords are shared between different inter-
actions of the web application with the web server and across
different users using the web application. When the web ap-
plication has started operating, these variables are initialized
to the null set. For example as shown in the State chart di-
agram of Figure 2, variables valid student usernames,
valid student passwords, valid teacher usernames and
Figure 1: Proposed Test Generation Method used valid teacher passwords are initialized to null set in the tran-
by our ACT tool sition from state Inactive to state Active. On a successful
registration of either a teacher or a student, the values of
these variables are updated and when either a student or
3. PROPOSED METHODOLOGY a teacher logs in the LMS Login page, the value of these
Figure 1 gives an overview of the approach that the ACT variables are accessed to check if a student or teacher is al-
(Abstract to Concrete test) tool uses for generating concrete ready registered or not. Our ACT tool, as illustrated in the
Selenium RC JUnit test cases from the formal State chart remaining sections can store and share data across different
web navigation model. The navigation behaviour of our case interactions of the web application with the web server and
study web application is modeled using the formal specifica- can generate Selenium RC JUnit concrete test cases utilizing
tion language ’State chart’. The front end which generates this data.
test paths from the State chart model can be a test path
generating algorithm like model checking or graph coverage 5. TEST PATH GENERATION FROM STATE
algorithm. Abstract test cases are generated from the test
paths with the help of the State chart specification. Then
CHART MODEL
the abstract test cases generated are converted to Selenium The front end step in the ACT tool which generates test
RC JUnit concrete test cases using the Mappings XML file. paths can be any test path generating algorithm like graph
Each of these steps are explained in elaborate details in the coverage algorithms. But model checking which is a formal
remaining sections. verification technique can also be used to generate test paths
by formulating a temporal logic specification as a trap prop-
4. A FORMAL MODEL FOR WEB NAVI- erty to be verified. The straight forward way to represent
a State chart as a transition system is to flatten its hierar-
GATION - STATE CHART chy. In our approach, the hierarchical State chart naviga-
From among the various finite state based formal specifica- tion model was first flattened and then transformed into an
tion languages, we have used Statecharts [1] for modeling the SMV program. The trap properties for navigation were writ-
navigation behaviour of web applications. Figure 2 shows ten in CTL formulas and then the Symbolic Model Verifier
the State chart specification of our case study, the Learn- (NuSMV) tool is executed which generates the counter ex-
ing Management System (LMS) used within our institute. amples. For example, the CTL Trap Specification Property
In the Statechart specification shown in Figure 2, Inactive for specifying that state SE-230 Software Testing is reach-
state denotes that the web application has not yet started able from the initial state is:
operating. The composite state Active denotes that the web
application is in an operating state. Inside Active state, each CTL Trap Specification Property:
web page was modelled as a separate state. When the user ! EF(state= SE-230 Software Testing)
navigates from one webpage to another, there is a transition
between the corresponding states. LMS Login Page denotes This trap property will generate a counter example which is
the Login page of Learning Management System. Here we our test path. For this counter example there will be two
have used the mathematical notations of sets and first order paths. One from LMS Login Page to My Courses Page to
predicate logic constructs in guards and actions of the tran- SE-230 Software Testing Page. And the second test path will
sitions in State chart model. In a web application, the value be the loop from LMS Login Page to Successfully Student
which is entered by the user in one interaction of the web Added Page then to My Course Page to SE-230 Software
application with the web server is often used back in another Testing page. Here we will restrict the length of the loop in
interaction of the web application with the web server. For the counter example by using bounded model checking and
example, as shown in the State chart model of Figure 2, ad- set the length of the counter example to a fixed size. The
min can register a student in the LMS System by entering CTL Trap properties for generating test paths are written
values in the username and password input fields in the Add for various requirements of the web application, like the top
Student User Page. A necessary requirement for a student page of a web application should be reachable from all the
to login in the LMS Login Page is that the student must be pages of the web application. In addition, we also wrote
registered beforehand and so must have a valid student user- CTL trap properties for node coverage criterion.
2nd Modelling Symposium (ModSym 2016) - colocated with ISEC 2016, Goa, India, Feb 18, 2016
17
!!! Initialize!/!
! valid_student_usernames=null/^/
! valid_student_passwords=null/^/
! valid_teacher_usernames=null/^/ Inactive!
!
valid_teacher_passwords=null/^/ shutdown!
valid_admin_username=``admin’’/^/
valid_admin_password=``admin’’/
Login.clicked/
Login.clicked/
Active! [!username!∉!valid_teacher_usernames/⋁!!!
[!username2!∉!valid_student_usernames/⋁!!!
!!password!!∉!valid_teacher_passwords!!!]!
!!password2!!∉!valid_student_passwords!!!]!
!
LMS!Login!Page!
!
Login.clicked/ Login.clicked/ Logout.clicked/
[!username2!∈!valid_student_usernames!!∧! [!username!=!valid_admin_username!/∧!/
password2!∈!valid_student_passwords!!]! !!!!password!=!valid_admin_password!]!
!
Login.clicked/
Logout.clicked/
[!username3!∈!!valid_teacher_usernames!/∧/
!!!password3!!∈!!valid_teacher_passwords!]!
!
! Admin!Home!!
My!Courses!!
Page!
Design/and/Analysis/
of/
Safety/Critical/ Software/ My!Courses! Add/
Systems.clicked/ Testing.clicked/ Users.clicked/
Add!Users!
CSISEI270!Design_and_Analysis!! SEI230_Software!
_Of_SafetyICritical_Systems! _Testing!
TDD/
Assignment.clicked/
Add/Teacher.clicked/ Add/
Grades.clicked/
Slides/ Student.clicked/
News/ Folder.clicked/
General/ Test!Driven!!
Forum.clicked/
Discussion/
Developemnt!
Grades!Page! Forum.clicked/
Assignment!Page!
Slides!Folder!
General!Discussion!!
News!Forum! page!
Forum!
Add!Teachers!! Add!Student!
User!Page! !User!Page!
Add.clicked/
Add.clicked/ [!username1!∉!valid_student_usernames!∧!
[!username1!∉ !"#$%_!"#$ℎ!"_!"#$%&'#"!∧! password1!∉!valid_student_passwords!]!/!
password1!∉ !"#$%_!"#$ℎ!"_!"##$%&'#!]!/! !
! valid_student_usernames/:=/
valid_teacher_usernames/:=/valid_teacher_usernames/// valid_student_usernames/∪/username///∧/
∪ !"#$%&'#!! ∧/ valid_student_passwords/:=/
valid_teacher_passwords/:=/valid_teacher_passwords/ Add.clicked/ valid_student_passwords/∪/password//
Add.clicked/
∪/password! /
/
[!username1!∈!!
[!username1!∈!
valid_teacher_usernames/∧!
valid_student_usernames!!∧!
password1!∈!
password1!∈!
valid_teacher_passwords!]!
valid_student_passwords!]!
Successfully!
Successfully!
Teacher!Added!!
Student!Added!
Page! Error!Page!
Page!
Figure 2: Formal Model showing Web Navigation of Learning Management System using UML State chart
model.
Test Criterion CTL Trap Property Description
A CTL Trap property for node
Node coverage ! EF (state=SE-230 Software Testing) coverage for state SE-230
Software Testing Page.
LMS Login Page is reachable
! AG((state=SE-230 Software Testing) →
The top page is reachable from all the pages from SE-230 Software Testing
EF(state=LMS Login Page))
Page.
SE-230 Software Testing Page is
! AG ((state=LMS Login Page) → EF
Every page is reachable from the top page reachable from LMS Login Page
(state=SE-230 Software Testing))
page.
Table 1: Some CTL Trap Temporal Logic Properties that were used for generating test paths from flattened
State chart model of Learning Management System in NuSMV tool.
2nd Modelling Symposium (ModSym 2016) - colocated with ISEC 2016, Goa, India, Feb 18, 2016
18
6. ABSTRACT TEST CASES GENERATION Symbolic
Execution Path
USING SYMBOLIC EXECUTION AND SMT Path Symbolic
Trace
Path
Predicate
Predicate
SMT
Spec Execution Solver
SOLVER Extraction
After the test paths are generated from the State chart Form Test
model, symbolic execution is carried out to generate input Abstract Test
Case
Concrete
values to guide the execution along the test paths. The path Case Generation Values
predicate corresponding to the test path is computed. This,
in turn, is given to an SMT solver to generate concrete input Abstract
Test
values. These values are used to generate the abstract test Case
cases. The algorithm used to generate the abstract test cases
using symbolic execution is shown in the block diagram in
Figure 3. Figure 3: Abstract test case generation using Sym-
bolic execution
6.1 Path Predicate Formation & Computation t1
of Concrete Values valid student usernames ← φ
valid student passwords ← φ
valid student usernames = φ
valid student passwords = φ
This section illustrates the method of formation of path s1
predicates and the generation of concrete values using the username ← “admin00
password ← “admin00
example of the counter example generated from the CTL Login.clicked
AddU sers.clicked username1
Trap Property !EF(state=SE-230 Software Testing). The AddStudent.clicked
username1 ← input()
password1
variables valid student usernames and valid student passwords password1 ← input()
Add.clicked()
in the State chart model in Figure 2 are internal program
variables and are internally maintained as sets. These vari-
ables are initialized to null in the transition from state In- t4
active to composite state Active as shown in Figure 2. The username1 ∈
password1 ∈
/ valid student usernames
/ valid student passwords
username1 ∈
password1 ∈
/φ
/φ
path predicate formed for the transition from Add Student
User Page to Successfully Student Added Page is
(username1 6= ””) ∧ (password1 6= ””) ∧ (username1 ∈ / valid student usernames ← valid student usernames
φ) ∧ (password1 ∈ / φ). ∪{username1}
valid student passwords ← valid student passwords
valid student usernames = {username1}
valid student passwords = {password1}
∪{password1}
Logout.clicked
Sets valid student usernames and valid student passwords are
consequently updated to username1 and password1. So the s3
path predicate for the transition from state LMS Login Page username2 ← input()
username2
password2 ← input()
password2
to My Courses is ((username1 Login.clicked()
6= ””∧(password1 6= ””)∧(username1 ∈ / φ)∧(password1 ∈ /
φ)∧(username2 ∈ username1)∧(password2 ∈ password1)) t5
So the final path predicate for the counter example username2 ∈ valid student usernames username2 ∈ {username1}
! EF(state=SE-230 Software Testing ) is: ((username1 6= password2 ∈ valid student passwords password2 ∈ {password1}
”” ∧ (password1 6= ””) ∧ (username1 ∈ / φ) ∧ (password1 ∈ /
φ) ∧ (username2 ∈ username1)∧ (a) (b)
(password2 ∈ password1))
Here username1 and password1 are the symbolic variables
corresponding to the Add Student User page, and username2 Figure 4: Symbolic Execution: (a) Control flow
and password2 are the symbolic variables corresponding to path; (b) Symbolic Execution Trace
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 corresponding GUI elements in system implementation are
occurring in the formula and hence the concrete input values extracted in sequence and their user input fields are replaced
would be generated. Suppose, if a counter example is gen- by concrete values computed in symbolic execution stage.
erated 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 7. TRANSLATION OF ABSTRACT TEST
will be: (username1 ∈ φ) ∧ (password1 ∈ φ) which will be CASES TO CONCRETE TEST CASES
a contradiction i.e. unsatisfiable predicate. Hence, this path
will be rejected as infeasible. The last step is deriving concrete executable test cases from
these abstract test cases so these concrete test cases can
6.2 Abstract Test Cases Generation communicate directly with the system under test. The ab-
stract test cases generated from the State chart model are
Finally the abstract test cases are generated by plugging on the same level of abstraction as the model since the State
in concrete input values which are computed in the sym- chart model they are generated from contains only partial
bolic execution stage at appropriate points in the counter information of the implementation under test. In Figure 5,
examples. The phases in the counter examples which have even through the input values are concrete, the test case is
2nd Modelling Symposium (ModSym 2016) - colocated with ISEC 2016, Goa, India, Feb 18, 2016
19
username=“admin”
password=“admin”
Login.clicked
Add Users.clicked
state
Add Student.clicked
Add Student User
username1=“MS2013009”
password1=“abc”
selenium=new DefaultSelenium(“localhost”,4444,”firefox/”
Add.clicked
+“Applications/Fire-
Logout.clicked
fox.app/Contents/MacOS/” +“firefox-
username2=“MS2013009”
bin”,“https://lms.iiitb.ac.in/moodle”);”
password2=“abc”
selenium.start();
Login.clicked
selenium.open(“/course/view.php?id=19”);
Software Testing.clicked
Figure 5: An example of an abstract test case gen-
username1
erated for the counter example generated from the u1
CTL Trap Temporal Logic Property !EF(state=SE- non blank
230 Software Testing) selenium.type (“css=input[id=’username’,]”,u1);
Name
still abstract because firstly variables like username1, pass- n
word1, etc. needs to be mapped to the implementation enti- selenium.type(“css=input[id=’name’]”,n);
ties . And, secondly many of the inputs that may be needed
may not be there in the original specification and are only Department
available after the exact implementation is finished. For dp
generating concrete test cases from the abstract test cases selenium.type(“css=input[id=’department’]”,dp);
generated in the previous step, the ACT tool uses a map-
ping 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 Figure 6: A part of Mappings XML file showing
JUnit test. Figure 8 shows a part of XML file that was cre- mappings between phrases used in State chart spec-
ated to give a mapping between the phrases in the State ification model of Figure 2 to their corresponding
chart model of Figure 2 to Selenium RC JUnit java code Selenium RC JUnit 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 system and a total of 53 abstract test cases were used for
were abstracted out from the State chart model has to be SIS System for various test criterion. Currently, we have
added in the Mappings XML file in order to generate the modelled the two case studies of HMS System and SIS Sys-
concrete Selenium RC Junit test cases. From the source tem but we are currently running our ACT tool and trying
code implementation of the case study of HMS, we found to calculate the number of concrete test cases that would be
that in the Add Student User page there were additional in- generated.
put 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
9. CONCLUSION
the mappings XML file created manually and fed as input Test cases generated from formal specifications are often at
to the ACT tool, a set of concrete Selenium RC Junit test an abstract level. They cannot be executed directly using a
cases is generated in this step. Figure 5 shows one of the test automation tool, e.g. Selenium. The existing methods
concrete Selenium JUnit test case generated from our ACT have tried to deal with this problem using a mapping ap-
tool for the case study of Learning Management System. proach. 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 be-
tween atomic interactions between the (test-)client and the
server. In this paper, we have presented a precise charac-
8. RESULTS terisation of this problem. Further, we have provided a test
generation methodology which uses symbolic execution to
For two other web based enterprise applications developed resolve the data-flow between atomic interaction. The re-
within our institute, a Hospital Management System (HMS) sulting abstract test cases are concrete enough so that the
and a Student Information System (SIS), we modeled our mapping method is effective in completely translating them
web applications using the proposed method. to concrete test cases that can be directly executed on Sele-
nium test runner. Through some of the steps like creation
Table 2 shows the lines of code (LOC) of the two systems, of Mappings XML file, construction of State chart, etc are
the number of nodes in the flattened State chart (Nf lat ), the manual but there is fairly a reasonable automation in the
number of mappings and the number of abstract test cases( other steps in the ACT tool. Therefore, our approach is
or counter examples) used for the various test coverage cri- able to achieve a reasonable amount of end to end automa-
terion. A total of 14 abstract test cases were used for HMS tion of the test generation process from formal specification.
2nd Modelling Symposium (ModSym 2016) - colocated with ISEC 2016, Goa, India, Feb 18, 2016
20
No. of abstract tests
Web Applications Nf lat LOC No. of Mappings
(counter examples)
Hospital Management Sys-
6 133 Node coverage 6
tem (HMS)
20 Top page is reachable from all the pages 4
Every page is reachable from the top page 4
Total 14
Student Information System
19 15,770 56 Node coverage 19
(SIS)
Top page is reachable from all the pages 17
Every page is reachable from the top page 17
Total 53
Table 2: Results of test generation on two other case studies Hospital Management System and Student
Information System
10. FUTURE WORK Intl. Conf. on Software Testing, Verification, and
Validation, pp. 121-130.
In our future work, we will try to address the following is-
[9] H. S. Hong, I. Lee, O. Sokolsky, “Automatic Test
sues:
Generation from Statecharts Using Model Checking”,
• Currently we are running our ACT tool on our LMS in Proc. of FATES’01, Workshop on Formal
system and we are currently trying to find out the Approaches to Testing of Software, Vol. NS-01-4 of
number of concrete test cases that would be generated BRICS Notes Series.
for various test criteria. So in our future work, we [10] S. Gnesi, D. Latella, and M. Massink, “Formal
will try to find out the relation between the number Test-Case Generation for UML Statecharts,” Proc.
of concrete test cases and the number of abstract test Ninth IEEE International Conf. Eng. of Complex
cases and we will also try to see how the number of Computer Systems, P. Bellini, S. Bohner, and B.
concrete test case and the number of abstract test cases Steffen, eds., Apr. 2004.
varies with the size of the State chart model. [11] CVC3 SMT solver: “http://www.cs.nyu.edu/acsys/
• In our future work, we will generalise this approach to cvc3/”
apply other forms of formal specification 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. REFERENCES
[1] D. Harel,“Statecharts: A Visual formalism for complex
systems”, Science of Computer Programming, Volume
8, Issue 3, June 1, 1987, Pages-231-274.
[2] K. Homma, S. Izumi, K. Takahashi and A.
Togashi,“Modeling and Verification of Web
Applications Using Formal Approach”. IEICE Tech.
Report, 2009.
[3] M. Han,C. Hofmeister,“Modeling and Verification of
Adaptive Navigation in Web Applications”, Proc. of
6th Intl. Conf. on Web Engg., pp. 329-336.
[4] F. Ricca, and P. Tonella, “Analysis and Testing of
Web Applications”, Proc. of the 23rd Intl. Conf. on
Software Engineering, pp. 25-34, 2001.
[5] M. H. Alalfi, J. R.Cordy, T. R.Dean,“Modeling
methods for Web Application Verification and Testing:
State of the art”, Software Testing, Verification and
Relaibility, Vol. 19, Issue 4, pp. 265-296.
[6] N. Li, J. Offutt, “A Test Automation Language for
Behavioral Models”, Technical Report,
GMU-CS-TR-2013-7.
[7] A.-M. Torsel, “A Testing Tool for Web Applications
Using a Domain-Specific Modelling Language and the
NuSMV Model Checker”, 6th Intl. Conf. on Software
Testing, Verification and Validation, pp. 383-390.
[8] A. Marcetto, P. Tonella, and F. Ricca, “State-based
Testing of AJAX Web Applications”, in Proc. of 2008
2nd Modelling Symposium (ModSym 2016) - colocated with ISEC 2016, Goa, India, Feb 18, 2016
21
public void test1 ()
{
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 ’)] " );
}
Figure 7: A Selenium RC JUnit concrete test case
generated from our ACT tool for the case study of
Learning Management System for the test path gen-
erated from the CTL trap property !EF(state= SE-
230 Software Testing)
2nd Modelling Symposium (ModSym 2016) - colocated with ISEC 2016, Goa, India, Feb 18, 2016
22