An Automated (F) LTL Test Oracle for Testing with Requirements

Ingo Pill, Franz Wotawa

Research output: Conference proceeding/Chapter in Book/Report/Conference Paperpeer-review

Abstract

Especially for safety-critical systems, we might want to express desired system properties in precise formal requirements. Verifying that a system then adheres to these requirements is obviously quite crucial. Complementing related methods like model checking or runtime monitors, for testing and most importantly debugging recognized problems, we would certainly be interested in automated test oracles for deriving program spectra. Such program spectra containing the details of the executions and the oracle's verdicts have been shown to be an effective reasoning basis for debugging purposes. In this paper, we show how to automatically derive such a test oracle via a special satisfiability encoding. In particular, we instantiate a dedicated SAT problem in conjunctive normal form directly from the requirements and a test case's execution data. As our experiments illustrate, our approach shows attractive performance and can be fully automated.
Original languageEnglish
Title of host publication2016 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW)
Pages197-204
Number of pages8
DOIs
Publication statusPublished - 27 Oct 2016
Externally publishedYes
Event2016 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW) - Ottawa, ON, Canada
Duration: 23 Oct 201627 Oct 2016

Conference

Conference2016 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW)
Period23/10/1627/10/16

Keywords

  • Semantics
  • Brakes
  • Testing
  • Encoding
  • Automobiles
  • Debugging
  • Context

Fingerprint

Dive into the research topics of 'An Automated (F) LTL Test Oracle for Testing with Requirements'. Together they form a unique fingerprint.

Cite this