Proceedings of ISP RAS


Usability of AutoProof: a case study of software verification

Mansur Khazeev (Innopolis University, Software Engineering Lab, Innopolis, Russia)
Victor Rivera (Innopolis University, Software Engineering Lab, Innopolis, Russia)
Manuel Mazzara (Innopolis University, Software Engineering Lab, Innopolis, Russia)
Alexander Tchitchigin (Innopolis University, Software Engineering Lab, Innopolis, Russia)

Abstract

Verification tools are often the result of several years of research effort. The development happens as a distributed effort inside academic institutes relying on the ability of senior investigators to ensure continuity. Quality attributes such as usability are unlikely to be targeted with the same accuracy required for commercial software where those factors make a financial difference. In order for such tools to become of widespread use, it is therefore necessary to spend an extra effort and attention on users' experience, and allow software engineers to benefit out of them without the necessity of understanding the mathematical machinery in full detail. In order to put the spotlight on usability of verification tools we chose an automated verifier for the Eiffel programming language, AutoProof, and a well-known benchmark, the Tokeneer problem. The tool is used to verify parts of the implementation of the Tokeneer so to identify AutoProof's strengths and weaknesses, and finally propose the necessary updates. The results show the efficacy of the tool in verifying a real piece of software and automatically discharging nearly two thirds of verification conditions. At the same time, the case study shows the demand for improved documentation and emphasizes the need for improvement in the tool itself and in the Eiffel IDE.

Keywords

static verification; formal specification; Eiffel, Autoproof; Design by Contract

Edition

Proceedings of the Institute for System Programming, vol. 28, issue 2, 2016, pp. 111-126.

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

DOI: 10.15514/ISPRAS-2016-28(2)-7

Full text of the paper in pdf Back to the contents of the volume