Change search
ReferencesLink to record
Permanent link

Direct link
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 (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.
, 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
URN: urn:nbn:se:kth:diva-40871DOI: 10.1007/978-3-642-24580-0_8ISI: 000307927100008ScopusID: 2-s2.0-81255165659OAI: diva2:442577
23rd IFIP International Conference on Testing Software and Systems

The final publication is available at 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.
Trita-CSC-A, ISSN 1653-5723 ; 2011:15
Testing, Machine learning, Symbolic constraint solving, Model checking
National Category
Computer Science
urn:nbn:se:kth:diva-41932 (URN)978-91-7501-117-2 (ISBN)
2011-11-07, Sal F3, Lindstedtsvägen 26 KTH, Stockholm, 13:00 (English)
QC 20111012Available from: 2011-10-12 Created: 2011-10-03 Last updated: 2011-10-12Bibliographically approved

Open Access in DiVA

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

Other links

Publisher's full

Search in DiVA

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

Search outside of DiVA

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

Altmetric score

Total: 264 hits
ReferencesLink to record
Permanent link

Direct link