Synthesizing Adaptive Test Strategies from Temporal Logic Specifications

Roderick Bloem, Robert Könighofer, Ingo Hans Pill, Franz Röck

Publikation: KonferenzbeitragPaperForschungBegutachtung

Abstract

Constructing good test cases is difficult and timeconsuming,
especially if the system under test is still under
development and its exact behavior is not yet fixed. We propose
a new approach to compute test cases for reactive systems from
a given temporal logic specification. The tests are guaranteed
to reveal certain simple bugs (like occasional bit-flips) in every
realization of the specification and for every behavior of the
uncontrollable part of the system’s environment. We aim at
unveiling faults for the lowest of four fault occurrence frequencies
possible (ranging from a single occurrence to persistence). Based
on well-established hypotheses from fault-based testing, we argue
that such tests are also sensitive for more complex bugs. Since
the specification may not define the system behavior completely,
we use reactive synthesis algorithms (with partial information) to
compute adaptive test strategies that react to behavior at runtime.
We work out the underlying theory and present first experiments
demonstrating that our approach can be applied to industrial
specifications and that the resulting strategies are capable of
detecting bugs that are hard to detect with random testing.
Originalspracheenglisch
Seiten17-24
Seitenumfang8
PublikationsstatusVeröffentlicht - 2016
VeranstaltungFormal Methods in Computer Aided Design 2016 - Mountain View, Ca., USA / Vereinigte Staaten
Dauer: 3 Okt 20166 Okt 2016

Konferenz

KonferenzFormal Methods in Computer Aided Design 2016
KurztitelFMCAD
LandUSA / Vereinigte Staaten
OrtMountain View, Ca.
Zeitraum3/10/166/10/16

Fingerprint

Temporal logic
Specifications
Testing

Dies zitieren

Bloem, R., Könighofer, R., Pill, I. H., & Röck, F. (2016). Synthesizing Adaptive Test Strategies from Temporal Logic Specifications. 17-24. Beitrag in Formal Methods in Computer Aided Design 2016, Mountain View, Ca., USA / Vereinigte Staaten.

Synthesizing Adaptive Test Strategies from Temporal Logic Specifications. / Bloem, Roderick; Könighofer, Robert; Pill, Ingo Hans; Röck, Franz.

2016. 17-24 Beitrag in Formal Methods in Computer Aided Design 2016, Mountain View, Ca., USA / Vereinigte Staaten.

Publikation: KonferenzbeitragPaperForschungBegutachtung

Bloem, R, Könighofer, R, Pill, IH & Röck, F 2016, 'Synthesizing Adaptive Test Strategies from Temporal Logic Specifications' Beitrag in, Mountain View, Ca., USA / Vereinigte Staaten, 3/10/16 - 6/10/16, S. 17-24.
Bloem R, Könighofer R, Pill IH, Röck F. Synthesizing Adaptive Test Strategies from Temporal Logic Specifications. 2016. Beitrag in Formal Methods in Computer Aided Design 2016, Mountain View, Ca., USA / Vereinigte Staaten.
Bloem, Roderick ; Könighofer, Robert ; Pill, Ingo Hans ; Röck, Franz. / Synthesizing Adaptive Test Strategies from Temporal Logic Specifications. Beitrag in Formal Methods in Computer Aided Design 2016, Mountain View, Ca., USA / Vereinigte Staaten.8 S.
@conference{829c64c10b684c99b610d8059ff3ace0,
title = "Synthesizing Adaptive Test Strategies from Temporal Logic Specifications",
abstract = "Constructing good test cases is difficult and timeconsuming,especially if the system under test is still underdevelopment and its exact behavior is not yet fixed. We proposea new approach to compute test cases for reactive systems froma given temporal logic specification. The tests are guaranteedto reveal certain simple bugs (like occasional bit-flips) in everyrealization of the specification and for every behavior of theuncontrollable part of the system’s environment. We aim atunveiling faults for the lowest of four fault occurrence frequenciespossible (ranging from a single occurrence to persistence). Basedon well-established hypotheses from fault-based testing, we arguethat such tests are also sensitive for more complex bugs. Sincethe specification may not define the system behavior completely,we use reactive synthesis algorithms (with partial information) tocompute adaptive test strategies that react to behavior at runtime.We work out the underlying theory and present first experimentsdemonstrating that our approach can be applied to industrialspecifications and that the resulting strategies are capable ofdetecting bugs that are hard to detect with random testing.",
author = "Roderick Bloem and Robert K{\"o}nighofer and Pill, {Ingo Hans} and Franz R{\"o}ck",
year = "2016",
language = "English",
pages = "17--24",
note = "Formal Methods in Computer Aided Design 2016, FMCAD ; Conference date: 03-10-2016 Through 06-10-2016",

}

TY - CONF

T1 - Synthesizing Adaptive Test Strategies from Temporal Logic Specifications

AU - Bloem, Roderick

AU - Könighofer, Robert

AU - Pill, Ingo Hans

AU - Röck, Franz

PY - 2016

Y1 - 2016

N2 - Constructing good test cases is difficult and timeconsuming,especially if the system under test is still underdevelopment and its exact behavior is not yet fixed. We proposea new approach to compute test cases for reactive systems froma given temporal logic specification. The tests are guaranteedto reveal certain simple bugs (like occasional bit-flips) in everyrealization of the specification and for every behavior of theuncontrollable part of the system’s environment. We aim atunveiling faults for the lowest of four fault occurrence frequenciespossible (ranging from a single occurrence to persistence). Basedon well-established hypotheses from fault-based testing, we arguethat such tests are also sensitive for more complex bugs. Sincethe specification may not define the system behavior completely,we use reactive synthesis algorithms (with partial information) tocompute adaptive test strategies that react to behavior at runtime.We work out the underlying theory and present first experimentsdemonstrating that our approach can be applied to industrialspecifications and that the resulting strategies are capable ofdetecting bugs that are hard to detect with random testing.

AB - Constructing good test cases is difficult and timeconsuming,especially if the system under test is still underdevelopment and its exact behavior is not yet fixed. We proposea new approach to compute test cases for reactive systems froma given temporal logic specification. The tests are guaranteedto reveal certain simple bugs (like occasional bit-flips) in everyrealization of the specification and for every behavior of theuncontrollable part of the system’s environment. We aim atunveiling faults for the lowest of four fault occurrence frequenciespossible (ranging from a single occurrence to persistence). Basedon well-established hypotheses from fault-based testing, we arguethat such tests are also sensitive for more complex bugs. Sincethe specification may not define the system behavior completely,we use reactive synthesis algorithms (with partial information) tocompute adaptive test strategies that react to behavior at runtime.We work out the underlying theory and present first experimentsdemonstrating that our approach can be applied to industrialspecifications and that the resulting strategies are capable ofdetecting bugs that are hard to detect with random testing.

UR - http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD16/proceedings.html

M3 - Paper

SP - 17

EP - 24

ER -