TY - JOUR
T1 - Automated generation of (F)LTL oracles for testing and debugging
AU - Pill, Ingo
AU - Wotawa, Franz
PY - 2018
Y1 - 2018
N2 - 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.
AB - 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.
U2 - 10.1016/j.jss.2018.02.002
DO - 10.1016/j.jss.2018.02.002
M3 - Article
VL - 139
SP - 124
EP - 141
JO - Journal of Systems and Software
JF - Journal of Systems and Software
SN - 0164-1212
ER -