ADVERTISEMENT

Home|Journals|Articles by Year|Audio Abstracts
 

Original Article

JJCIT. 2015; 1(Jordanian Journal of Computers and Information Technology, Vol. 1, No. 1, 2015): 15-30


Using Formal Methods for Test Case Generation According to Transition-Based Coverage Criteria

Ahmad A. Saifan, Wafa Bani Mustafa.




Abstract

- Formal methods play an important role in increasing the quality, reliability, robustness and effectiveness of software. Also the uses of formal methods, especially in safety-critical systems, help in the early detection of software errors and failures which will reduce the cost and effort involved in software testing.
The aim of this paper is to prove the role and the effectiveness of formal specification for the cruise control system (CCS) as a case study. A CCS formal model is built using Perfect formal specification language, and its correctness is validated using the Perfect Developer toolset. We develop a software testing tool in order to generate test cases using three different algorithms. These test cases are evaluated to improve their coverage and effectiveness. The results show that random test case generation with full restriction algorithm is the best in its coverage results; the average of the path coverage is 77.78% and the average of the state coverage is 100%. Finally, our experimental results show that Perfect formal specification language is appropriate to specify CCS which is one of the most safety-critical software systems, so the process of detecting all future possible cases becomes easier.

Key words: Formal Method, Perfect Developer, test case generation, cruise control system







Plum Print visual indicator of research metrics
  • Citations
    • Citation Indexes: 3
  • Captures
    • Readers: 6
see details

Bibliomed Article Statistics

8
13
7
13
15
14
31
12
39
35
44
33
R
E
A
D
S

17
19
11
28
11
17
21
25
8
20
24
22		D
O
W
N
L
O
A
D
S
050607080910111201020304
20242025

Full-text options


Share this Article


Online Article Submission
• ejmanager.com


ejPort - eJManager.com
Author Tools
 About BiblioMed
License Information
Terms & Conditions
Privacy Policy
 Contact Us

The articles in Bibliomed are open access articles licensed under Creative Commons Attribution 4.0 International License (CC BY), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.


We use cookies and other tracking technologies to work properly, to analyze our website traffic, and to understand where our visitors are coming from. More Info Got It!