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 language | English |
---|---|
Title of host publication | 2016 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW) |
Pages | 197-204 |
Number of pages | 8 |
DOIs | |
Publication status | Published - 27 Oct 2016 |
Externally published | Yes |
Event | 2016 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW) - Ottawa, ON, Canada Duration: 23 Oct 2016 → 27 Oct 2016 |
Conference
Conference | 2016 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW) |
---|---|
Period | 23/10/16 → 27/10/16 |
Keywords
- Semantics
- Brakes
- Testing
- Encoding
- Automobiles
- Debugging
- Context