Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Learning-based Software Testing using Symbolic Constraint Solving Methods
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
2011 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Software testing remains one of the most important but expensive approaches to ensure high-quality software today. In order to reduce the cost of testing, over the last several decades, various techniques such as formal verification and inductive learning have been used for test automation in previous research.

In this thesis, we present a specification-based black-box testing approach, learning-based testing (LBT), which is suitable for a wide range of systems, e.g. procedural and reactive systems. In the LBT architecture, given the requirement specification of a system under test (SUT), a large number of high-quality test cases can be iteratively generated, executed and evaluated by means of combining inductive learning with constraint solving.

We apply LBT to two types of systems, namely procedural and reactive systems. We specify a procedural system in Hoare logic and model it as a set of piecewise polynomials that can be locally and incrementally inferred. To automate test case generation (TCG), we use a quantifier elimination method, the Hoon-Collins cylindric algebraic decomposition (CAD), which is applied on only one local model (a bounded polynomial) at a time.

On the other hand, a reactive system is specified in temporal logic formulas, and modeled as an extended Mealy automaton over abstract data types (EMA) that can be incrementally learned as a complete term rewriting system (TRS) using the congruence generator extension (CGE) algorithm. We consider TCG for a reactive system as a bounded model checking problem, which can be further reformulated into a disunification problem and solved by narrowing.

The performance of the LBT frameworks is empirically evaluated against random testing for both procedural and reactive systems (executable models and programs). The results show that LBT is significantly more efficient than random testing in fault detection, i.e. less test cases and potentially less time are required than for random testing.

Place, publisher, year, edition, pages
Stockholm: KTH Royal Institute of Technology , 2011. , vii, 47 p.
Series
Trita-CSC-A, ISSN 1653-5723 ; 2011:15
Keyword [en]
Testing, Machine learning, Symbolic constraint solving, Model checking
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-41932ISBN: 978-91-7501-117-2 (print)OAI: oai:DiVA.org:kth-41932DiVA: diva2:445529
Presentation
2011-11-07, Sal F3, Lindstedtsvägen 26 KTH, Stockholm, 13:00 (English)
Opponent
Supervisors
Note
QC 20111012Available from: 2011-10-12 Created: 2011-10-03 Last updated: 2011-10-12Bibliographically approved
List of papers
1. A Learning-based Approach to Unit Testing of Numerical Software
Open this publication in new window or tab >>A Learning-based Approach to Unit Testing of Numerical Software
2010 (English)In: 22nd IFIPInternational Conference on Testing Software and Systems, Natal, Brazil, Nov. 8-12, 2010 / [ed] Alexandre Petrenko, Adenilso da Silva Simão, José Carlos Maldonado, Berlin, Heidelberg: Springer , 2010, 221-235 p.Conference paper, Published paper (Refereed)
Abstract [en]

We present an application of learning-based testing to theproblem of automated test case generation (ATCG) for numerical soft-ware. Our approach uses n-dimensional polynomial models as an algo-rithmically learned abstraction of the SUT which supports n-wise testing.Test cases are iteratively generated by applying a satisfiability algorithmto first-order program specifications over real closed fields and iterativelyrefined piecewise polynomial models.We benchmark the performance of our iterative ATCG algorithm againstiterative random testing, and empirically analyse its performance in find-ing injected errors in numerical codes. Our results show that for softwarewith small errors, or long mean time to failure, learning-based testing isincreasingly more efficient than iterative random testing.

Place, publisher, year, edition, pages
Berlin, Heidelberg: Springer, 2010
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 6435
Keyword
Machine learning, Software Testing, Model Checking
National Category
Computer Science
Identifiers
urn:nbn:se:kth:diva-40870 (URN)10.1007/978-3-642-16573-3_16 (DOI)000289226300016 ()2-s2.0-78649885303 (Scopus ID)978-3-642-16572-6 (ISBN)
Available from: 2011-09-26 Created: 2011-09-21 Last updated: 2011-10-12Bibliographically approved
2. Learning-Based Testing for Reactive Systems using Term Rewriting Technology
Open this publication in new window or tab >>Learning-Based Testing for Reactive Systems using Term Rewriting Technology
2011 (English)In: Proceedings of the 22nd IFIP International Conference on Testing Software and Systems, Paris, France, November 7-9, 2011 / [ed] B. Wolff and F. Zaidi, Berlin, Heidelberg: Springer , 2011, 97-114 p.Conference paper, Published paper (Refereed)
Abstract [en]

We show how the paradigm of learning-based testing (LBT) can be applied to automate specification-based black-box testing of reactive systems using term rewriting technology. A general model for a reactive system can be given by an extended Mealy automata (EMA) over an abstract data type (ADT).A finite state EMA over an ADT can be efficiently learned in polynomial time using the CGE regular inference algorithm, which builds a compact representation as a complete term rewriting system. We show how this rewriting system can be used to model check the learned automaton against a temporal logic specification by means of narrowing. Combining CGE learning with a narrowing model checker we obtain a new and general architecture for learning-based testing of reactive systems. We compare the performance of this LBT architecture against random testing using a case study.

Place, publisher, year, edition, pages
Berlin, Heidelberg: Springer, 2011
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 7019
Keyword
Software testing, Model checking, Term rewriting, Symbolic computation, Machine learning
National Category
Computer Science
Identifiers
urn:nbn:se:kth:diva-40871 (URN)10.1007/978-3-642-24580-0_8 (DOI)000307927100008 ()2-s2.0-81255165659 (Scopus ID)
Conference
23rd IFIP International Conference on Testing Software and Systems
Note

The final publication is available at www.springerlink.com QC 20110930

Available from: 2011-09-30 Created: 2011-09-21 Last updated: 2013-04-19Bibliographically approved

Open Access in DiVA

fulltext(1654 kB)810 downloads
File information
File name FULLTEXT02.pdfFile size 1654 kBChecksum SHA-512
a6bdbc32852adc4312c23630080326c0bbb220b085650eae97700735f81132386639974a575834857157e540e880778f4c1363e5e8c9aec5433ed317d1783f86
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Niu, Fei
By organisation
Theoretical Computer Science, TCS
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 814 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 1542 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf