Model-based Abductive Reasoning in Automated Software Testing

Automated Software Testing (AST) using Model Checking is in this paper epistemologically analysed in order to argue in favour of a model-based reasoning paradigm in computer science. Preliminarily, it is shown how both deductive and inductive reasoning are insufficient to determine whether a given piece of software is correct with respect to specified behavioural properties. Models algorithmically checked in Model Checking to select executions to be observed in Software Testing are acknowledged as analogical models establishing isomorphic relations with the target system’s data set. Analogical models in AST are presented as abductive models providing hypothetical explanations of observed executions. The model assumption - algorithmic check - software testing process is understood as the abduction - deduction - induction process defining the selective abduction and turned to isolate a set of model-based hypotheses concerning the target system behaviours. A manipulative abduction process is finally recognized in the practice of adapting, abstracting, and refining models that do not provide successful predictions.