Proceedings of ISP RAS

Model-based testing of Internet Mail Protocols.

N.V. Pakulin, A.N. Tugaenko.


The paper discusses model-based testing of the modern Internet e-mail protocols, including the method of protocol modeling by means of formal notations, peculiarities of e-mail protocols in the context of testing. The paper presents results of model-based testing of a number of popular open-source e-mail implementations. JavaTESK, an extension of Java programming language, was used to develop formal functional and test specifications for SMTP and POP3 protocols. The developed test suite includes separate tests for SMPT and POP3 as well as integration test for composition of SMTP and POP3 in a single implementation.


formal methods, verification, testing, email protocols, UniTESK


Proceedings of the Institute for System Programming, vol. 20, 2011, pp. 125-141.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

Full text of the paper in pdf (in Russian) Back to the contents of the volume