Genetic Synthesis of Concurrent Code Using Model Checking and Statistical Model Checking

Genetic programming (GP) is a heuristic method for automatically generating code. It applies probabilistic-based generation and mutation of code, combined with "natural selection" principles, using a fitness function. Often, the fitness is calculated based on a large test suite. Recently, GP was applied for synthesizing correct-by-design concurrent code from temporal specification, where model checking was used for calculating the fitness function. A deficiency of this approach is that it uses a limited number of fitness values, based on a small number of modes for each verified specification property (e.g., satisfies, does not satisfy a given property). Furthermore, the need to apply model checking on many candidate solutions using the genetic process makes using an off-the-shelf model checker such as Spin prohibitively expensive. The repeated invocation of such a tool, compiling the code for a new candidate solution and running it, can render the performance of this approach several orders of magnitude slower than using an internal model checking. To tackle this problem, we describe here the use of a combination of statistical model checking, and a light use of model checking, for calculating the fitness required by GP.