Automated generation of (F)LTL oracles for testing and debugging

For being able to draw on automated reasoning that helps us in improving the quality of some software artifact or cyber-physical system, we have to express desired system traits in precise formal requirements. Verifying that a system adheres to these requirements allows us then to gain the crucial level of confidence in its capabilities and quality. Complementing related methods like model checking or runtime monitors, for testing and most importantly debugging recognized problems, we would certainly be interested in automated oracles. These oracles would allow us to judge whether observed (test) data really adhere to desired properties, and also to derive program spectra that have been shown to be an effective reasoning basis for debugging purposes. In this paper, we show how to automatically derive such an oracle as a dedicated satisfiability encoding that is specifically tuned to the considered test data at hand. In particular, we instantiate a dedicated SAT problem in conjunctive normal form directly from the requirements and a test case's execution data. Our corresponding experiments illustrate that our approach shows attractive performance and can be fully automated.