Formal Verification to Enhance Evolution of Protocols

This paper describes a combined evolutionary system whereby formal correctness properties are used to augment a standard functional fitness score. This system was applied to the problem of evolving the receive side of an alternating bit protocol, represented by a Petrinet. The fitness function combined a test for freedom from deadlock in addition to a functional scoring system. The efficiency gain produced nets of equal functional fitness requiring approximately one third of the number of evaluations required when functional tests were used alone. This result has wider applicability in any genetic programming evolution where formal correctness tests of the algorithms can be carried out.