Formal Verification to Enhance Evolution of Protocols

Tim Lewis; Russell Haines

doi:10.1145/1569901.1570219

Formal Verification to Enhance Evolution of Protocols

Tim Lewis, Russell Haines

School of Computer Science, Electrical and Electronic Engineering and Engineering Maths

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

1 Citation (Scopus)

Abstract

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 language	English
Title of host publication	ACM 11th Annual conference on Genetic and evolutionary computation
Subtitle of host publication	GECCO 09
Pages	1889-1890
DOIs	https://doi.org/10.1145/1569901.1570219
Publication status	Published - 8 Jul 2009

Access to Document

10.1145/1569901.1570219

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

Cite this

@inproceedings{7d7340026aa04e0cb63869683bafbb0b,

title = "Formal Verification to Enhance Evolution of Protocols",

abstract = "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.",

author = "Tim Lewis and Russell Haines",

year = "2009",

month = jul,

day = "8",

doi = "10.1145/1569901.1570219",

language = "English",

isbn = "978-1-60558-325-9",

pages = " 1889--1890",

booktitle = "ACM 11th Annual conference on Genetic and evolutionary computation",

}

TY - GEN

T1 - Formal Verification to Enhance Evolution of Protocols

AU - Lewis, Tim

AU - Haines, Russell

PY - 2009/7/8

Y1 - 2009/7/8

N2 - 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.

AB - 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.

U2 - 10.1145/1569901.1570219

DO - 10.1145/1569901.1570219

M3 - Conference Contribution (Conference Proceeding)

SN - 978-1-60558-325-9

SP - 1889

EP - 1890

BT - ACM 11th Annual conference on Genetic and evolutionary computation

ER -