NADA: Neural Acceptance-Driven Approximate Specification Mining

It is hard to mine high-quality finite-state automata (FSAs) only from desired software behaviors, i.e., positive examples, because of a search space explosion and an overgeneralization problem induced by a lack of undesired software behaviors, i.e., negative examples. To tackle the overgeneralization problem, we suggest modeling the problem as searching for approximate FSAs from positive and negative examples with noise, where the noise originates from synthetic negative examples used to reject overgeneralized results. To obtain an effective search bias in the exploding search space, we bridge FSA acceptance to neural network inference.

Our key contribution is to design a neural network whose parameter assignment corresponds to an FSA, and its neural inference process, named after neural acceptance, is able to simulate FSA acceptance. The neural acceptance provides a way to quantify how well an FSA fits noisy data efficiently. We propose NADA, a neural acceptance-driven approach, to search for approximate FSAs guided by accepting positive examples and rejecting synthetic negative examples. NADA is based on a proper continuous relaxation of the discrete search space of FSAs and an efficient gradient descent-based search algorithm. Experimental results demonstrate that, compared with state-of-the-art approaches, NADA significantly improves the quality of mined FSAs (on average improves 41.63% F1 score). Besides, NADA is 19.8X faster than the approach mining sub-high-quality FSAs. CCS Concepts: • Software and its engineering → Dynamic analysis; Software testing and debugging; • Computing methodologies → Neural networks; • Theory of computation → Modal and temporal logics.