Date of Award

2005

Publication Type

Master Thesis

Degree Name

M.Sc.

Department

Computer Science

Keywords

Computer Science.

Rights

info:eu-repo/semantics/openAccess

Abstract

Testing is one of the vital steps in software development process. To convey testing, test cases need to be generated to check whether an implementation conforms to the design specification. Design specifications are usually expressed as Extended Finite State Machines (EFSMs) and test cases are actually a path from the initial state to a specific state on that EFSM. One of the most difficult issues of test case generation for EFSMs comes from the fact that infeasible paths exist on EFSMs. Two approaches have been developed in earlier 90s' to generate feasible paths from EFSMs: one is to develop algorithm to search EFSMs directly to generate feasible paths, and the other is to expand EFSMs into Finite State Machines (FSMs), followed by applying FSM techniques to generate feasible paths. Model checking method was proposed recently as a new approach for test case generation. It has some advantages over previous methods such as efficiency on number of states explored. However, by nature, it also has some disadvantages such as time inefficiency. Here we present a comparison between the model checking method and the previous expansion method from pragmatic aspect by running experiments. To carry on this comparison, we implemented a classical expansion algorithm, defined the translation from EFSMs to Promela models, and used SPIN model checker in the model checking approach. We have run sufficient number of test case generation experiments, compared the two approaches on their time consumptions, numbers of states explored, performance changes when EFSMs' sizes increase etc. By this comparison, we can see the tradeoff between time consumptions and the number of states explored in the two approaches and observe their performance changes while EFSMs change. Finally, we show the existence of the trade-off between state efficiency and time efficiency of the two approaches, the impact of domain size of variable value, the native drawbacks of the expansion algorithm and the performance improvement by tuning Premela models.Dept. of Computer Science. Paper copy at Leddy Library: Theses & Major Papers - Basement, West Bldg. / Call Number: Thesis2005 .T36. Source: Masters Abstracts International, Volume: 44-03, page: 1415. Thesis (M.Sc.)--University of Windsor (Canada), 2005.

Download

Share

COinS