Validation of SDL specifications using EFSM-based test generation

W. Eric Wong, Andy Restrepo, Byoungju Choi

Research output: Contribution to journalArticlepeer-review

10 Scopus citations


Existing methods for testing an SDL specification mainly allow for either black box simulation or conformance testing to verify that the behavior of an implementation matches its corresponding model. However, this relies on the potentially hazardous assumption that the model is completely correct. We propose a test generation method that can accomplish conformance verification as well as coverage criteria-driven white box testing of the specification itself. We first reformat a set of EFSMs equivalent to the processes in an SDL specification and identify "hot spots" - nodes or edges in the EFSM which should be prioritized during testing to effectively increase coverage. Then, we generate test sequences intended to cover selected hot spots; we address the possible infeasibility of such a test sequence by allowing for its rejection decided by a constraint solver and re-generation of an alternate test sequence to the hot spot. In this paper, we present our test generation method and tool, and provide case studies on five SDL processes demonstrating the effectiveness of our coverage-based test sequence selection.

Original languageEnglish
Pages (from-to)1505-1519
Number of pages15
JournalInformation and Software Technology
Issue number11
StatePublished - Nov 2009

Bibliographical note

Funding Information:
This research was supported by the MKE (Ministry of Knowledge Economy), Korea, under the ITRC (Information Technology Research Center) support program supervised by the IITA (Institute of Information Technology Advancement): IITA-2007-(C1090-0801-0032).


  • Constraint solver
  • Coverage testing
  • Dominator analysis
  • EFSM (Extended Finite State Machine)
  • Hot spot
  • SDL


Dive into the research topics of 'Validation of SDL specifications using EFSM-based test generation'. Together they form a unique fingerprint.

Cite this