Usability of AutoProof: a case study of software verification
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...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Ivannikov Institute for System Programming of the Russian Academy of Sciences
2018-10-01
|
| Series: | Труды Института системного программирования РАН |
| Subjects: | |
| Online Access: | https://ispranproceedings.elpub.ru/jour/article/view/63 |
| _version_ | 1811286004908163072 |
|---|---|
| author | Mansur Khazeev Victor Rivera Manuel Mazzara Alexander Tchitchigin |
| author_facet | Mansur Khazeev Victor Rivera Manuel Mazzara Alexander Tchitchigin |
| author_sort | Mansur Khazeev |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-13T02:52:20Z |
| format | Article |
| id | doaj.art-760e5eda95164f7b8ad684a20546a68d |
| institution | Directory Open Access Journal |
| issn | 2079-8156 2220-6426 |
| language | English |
| last_indexed | 2024-04-13T02:52:20Z |
| publishDate | 2018-10-01 |
| publisher | Ivannikov Institute for System Programming of the Russian Academy of Sciences |
| record_format | Article |
| series | Труды Института системного программирования РАН |
| spelling | doaj.art-760e5eda95164f7b8ad684a20546a68d2022-12-22T03:05:48ZengIvannikov Institute for System Programming of the Russian Academy of SciencesТруды Института системного программирования РАН2079-81562220-64262018-10-0128211112610.15514/ISPRAS-2016-28(2)-763Usability of AutoProof: a case study of software verificationMansur Khazeev0Victor Rivera1Manuel Mazzara2Alexander Tchitchigin3Университет ИннополисУниверситет ИннополисУниверситет ИннополисУниверситет Иннополис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.https://ispranproceedings.elpub.ru/jour/article/view/63статическая верификация, формальная спецификация, eiffel, autoproof, контрактное программирование |
| spellingShingle | Mansur Khazeev Victor Rivera Manuel Mazzara Alexander Tchitchigin Usability of AutoProof: a case study of software verification Труды Института системного программирования РАН статическая верификация, формальная спецификация, eiffel, autoproof, контрактное программирование |
| title | Usability of AutoProof: a case study of software verification |
| title_full | Usability of AutoProof: a case study of software verification |
| title_fullStr | Usability of AutoProof: a case study of software verification |
| title_full_unstemmed | Usability of AutoProof: a case study of software verification |
| title_short | Usability of AutoProof: a case study of software verification |
| title_sort | usability of autoproof a case study of software verification |
| topic | статическая верификация, формальная спецификация, eiffel, autoproof, контрактное программирование |
| url | https://ispranproceedings.elpub.ru/jour/article/view/63 |
| work_keys_str_mv | AT mansurkhazeev usabilityofautoproofacasestudyofsoftwareverification AT victorrivera usabilityofautoproofacasestudyofsoftwareverification AT manuelmazzara usabilityofautoproofacasestudyofsoftwareverification AT alexandertchitchigin usabilityofautoproofacasestudyofsoftwareverification |