Skip to main content

Automated protocol synthesis from requirements

Supervisor

Suitable for

Abstract

Network protocols are sets of rules that define how information is exchanged between computers or agents on a network. Many communication protocols, to mention Bluetooth, can be modelled as timed automata or their extensions. Protocols typically have the same algorithmic structure but may differ in values of parameters, e.g. timing delays. This project aims to develop a method for synthesising protocols from requirements given in temporal logic so that they are correct by construction. The idea is to combine template-based synthesis (“Template-based Program Verification and Program Synthesis”, Journal on Software Tools for Technology Transfer, 2012) with parameter synthesis for timed automata developed and implemented recently (http://www.veriware.org/bibitem.php?key=DKKM14). This way, the algorithmic structure will be given as a parametric template, and appropriate parameter values can be selected automatically to optimise a given quantitative requirement. This project would suit a student interested in theory and/or constraint solving.