Formal Verification to Enhance Evolution of Protocols

Tim Lewis, Russell Haines

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

1 Citation (Scopus)


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.
Original languageEnglish
Title of host publicationACM 11th Annual conference on Genetic and evolutionary computation
Subtitle of host publicationGECCO 09
Pages 1889-1890
Publication statusPublished - 8 Jul 2009


Dive into the research topics of 'Formal Verification to Enhance Evolution of Protocols'. Together they form a unique fingerprint.

Cite this