Synthesizing adaptive test strategies from temporal logic specifications

Roderick Bloem, Goerschwin Fey, Fabian Greif, Robert Könighofer, Ingo Pill, Heinz Riener, Franz Röck*

*Korrespondierende/r Autor/in für diese Arbeit

Publikation: Beitrag in einer FachzeitschriftArtikel

Abstract

Constructing good test cases is difficult and time-consuming, 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 strategies for reactive systems from a given temporal logic specification using formal methods. The computed strategies are guaranteed to reveal certain simple faults in every realization of the specification and for every behavior of the uncontrollable part of the system’s environment. The proposed approach supports different assumptions on occurrences of faults (ranging from a single transient fault to a persistent fault) and by default aims at unveiling the weakest one. 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. The computed strategies are adaptive test strategies that react to behavior at runtime. We work out the underlying theory of adaptive test strategy synthesis and present experiments for a safety-critical component of a real-world satellite system. We demonstrate that our approach can be applied to industrial specifications and that the synthesized test strategies are capable of detecting bugs that are hard to detect with random testing.

Originalspracheenglisch
Seiten (von - bis)103-135
Seitenumfang33
FachzeitschriftFormal Methods in System Design
Jahrgang55
Ausgabenummer2
DOIs
PublikationsstatusVeröffentlicht - 2019

ASJC Scopus subject areas

  • Software
  • !!Theoretical Computer Science
  • !!Hardware and Architecture

Fields of Expertise

  • Information, Communication & Computing

Fingerprint

Untersuchen Sie die Forschungsthemen von „Synthesizing adaptive test strategies from temporal logic specifications“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren