Method of Network Protocol Specification Using the Haskell Language

Student: Volkov Grigoriy

Educational Programme: System Programming (Master)

Year of Graduation: 2020

Network protocols are usually specified informally in text documents. Formal specifications help automate the development, testing and implementation of protocols. During the development of a protocol implementation testing system at ISP RAS, we discovered that existing formal executable specification tools did not work very well for testing systems. In this paper, we introduce a new specification method for network protocol messages. The method includes a specification language (embedded in the Haskell programming language) based on type-level annotations, and methods for executing such specifications. The method was developed for use in both testing systems and protocol implementations. The main advantage of the method is that errors in the specification are detected at compile time, which makes specification development easier. This is accomplished using type-level programming in Haskell.

Student Theses at HSE must be completed in accordance with the University Rules and regulations specified by each educational programme.

Summaries of all theses must be published and made freely available on the HSE website.

The full text of a thesis can be published in open access on the HSE website only if the authoring student (copyright holder) agrees, or, if the thesis was written by a team of students, if all the co-authors (copyright holders) agree. After a thesis is published on the HSE website, it obtains the status of an online publication.

Student theses are objects of copyright and their use is subject to limitations in accordance with the Russian Federation’s law on intellectual property.

In the event that a thesis is quoted or otherwise used, reference to the author’s name and the source of quotation is required.

Search all student theses