Software model synthesis using satisfiability solv

Authors: Marijn J H Heule Sicco Verwer

Publish Date: 2012/08/09

Volume: 18, Issue: 4, Pages: 825-856

PDF Link

Abstract

We introduce a novel approach for synthesis of software models based on identifying deterministic finite state automata Our approach consists of three important contributions First we argue that in order to model software one should focus mainly on observed executions positive data and use the randomly generated failures negative data only for testing consistency We present a new greedy heuristic for this purpose and show how to integrate it in the stateoftheart evidencedriven statemerging EDSM algorithm Second we apply the enhanced EDSM algorithm to iteratively reduce the size of the problem Yet during each iteration the evidence is divided over states and hence the effectiveness of this algorithm is decreased We propose—when EDSM becomes too weak—to tackle the reduced identification problem using satisfiability solvers Third in case the amount of positive data is small we solve the identification problem several times by randomizing the greedy heuristic and combine the solutions using a voting scheme The interaction between these contributions appeared crucial to solve hard software models synthesis benchmarks Our implementation called DFASAT won the StaMinA competitionThe first author is supported by the Austrian Science Foundation FWF NFN Grant S11408N23 RiSE The second author is supported by STW project 11763 ITALIA and the Research Foundation Flanders FWOVlaanderen project G068211 Declarative experimentation

Keywords: