Contractor Validation Tool

All the files necessary for replaying this case studies are available in the examples section of this web site.

5. SMTPProtocol

Class source: Ristretto mail protocols library (Java)
Behaviour requirements source: Manually-generated model presented in a paper by Dallmeier et al. Paper and Model

The SMTPProtocol class is a Java implementation of an SMTP protocol client.

Contractor was ran and obtained its enabledness-preserving abstraction:

When compared to the manually-generated model depicted next, the reviewer discovered that our abstraction was more permissive.

In particular, the manually-generated model reflected a number of method ordering restrictions, such as requiring mails to be initiated (mail) before recipients could be added (rcpt).

On the other hand, our abstraction allowed recipients to be added anytime, as long as the connection with the server was established. This lack of restrictions in our abstraction is caused by the  SMTPProtocol implementation, which does not keep track of the current state and relies on the SMTP server side to raise an error in case actions are triggered in the wrong order.

This stateless SMTP client relies on a well implemented SMTP server to work properly. This server-side validation nature of the client is not reflected on the manually-generated model.

ICSE 2011 Manuscript Case Studies