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 Testing for Reactive Systems using Term Rewriting Technology
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-9706-5008
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
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. 97-114 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 7019
Keyword [en]
Software testing, Model checking, Term rewriting, Symbolic computation, Machine learning
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-40871DOI: 10.1007/978-3-642-24580-0_8ISI: 000307927100008Scopus ID: 2-s2.0-81255165659OAI: oai:DiVA.org:kth-40871DiVA: diva2:442577
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
In thesis
1. Learning-based Software Testing using Symbolic Constraint Solving Methods
Open this publication in new window or tab >>Learning-based Software Testing using Symbolic Constraint Solving Methods
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
Testing, Machine learning, Symbolic constraint solving, Model checking
National Category
Computer Science
Identifiers
urn:nbn:se:kth:diva-41932 (URN)978-91-7501-117-2 (ISBN)
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

Open Access in DiVA

KMFN2011(486 kB)359 downloads
File information
File name FULLTEXT01.pdfFile size 486 kBChecksum SHA-512
3ad85c28fbc20a4c830a6ece92ad3d490d27b1ce1fffbdb95d66e38636e87fa270730f4b480e18c64574f380c6f82d0e8282fbf6f02bfa18eb164422d81bd0d3
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopusSpringerlink.com

Authority records BETA

Meinke, Karl

Search in DiVA

By author/editor
Meinke, KarlNiu, Fei
By organisation
Theoretical Computer Science, TCS
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 359 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

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 314 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