Usability of AutoProof: a case study of software verification
Автор: Khazeev Mansur, Rivera Victor, Mazzara Manuel, Tchitchigin Alexander
Журнал: Труды Института системного программирования РАН @trudy-isp-ran
Статья в выпуске: 2 т.28, 2016 года.
Бесплатный доступ
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.
Static verification, formal specification, design by contract, eiffel, autoproof
Короткий адрес: https://sciup.org/14916333
IDR: 14916333 | DOI: 10.15514/ISPRAS-2016-28(2)-7
Список литературы Usability of AutoProof: a case study of software verification
- B. Meyer, Touch of Class: Learning to Program Well with Objects and Contracts. Springer Publishing Company, Incorporated, 1 ed., 2009.
- P. Cousot and R. Cousot, “Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints,” in Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’77, (New York, NY, USA), pp. 238-252, ACM, 1977.
- E. M. Clarke, Jr., O. Grumberg, and D. A. Peled, Model Checking. Cambridge, MA, USA: MIT Press, 1999.
- D. W. Loveland, Automated Theorem Proving: A Logical Basis (Fundamental Studies in Computer Science). sole distributor for the U.S.A. and Canada, Elsevier North-Holland, 1978.
- J. Tschannen, C. A. Furia, M. Nordio, and N. Polikarpova, “AutoProof: Auto-active functional verification of object-oriented programs,” in 21st International Conference, TACAS 2015, London, UK, April 11-18, 2015. Proceedings, pp. 566-580, 2015.
- B. Meyer, Object-oriented software construction, ch. 11: Design by Contract: building reliable software. Prentice Hall PTR, 1997.
- AdaCore, “Tokeneer.” http://www.adacore.com/sparkpro/tokeneer/download, accessed in April 2016.
- J.-R. Abrial, S. Schuman, and B. Meyer, “Specification Language,” in On the Construction of Programs, R. M. McKeag and A. M. Macnaghten, editors, pp. 343-410, Cambridge University Press, 1980.
- J. Barnes, High Integrity Software: The SPARK Approach to Safety and Security. Boston, MA, USA: Addison-Wesley Longman Publishing Co., Inc., 2003.
- K. R. M. Leino, “This is boogie 2,” tech. rep., June 2008.
- N. Polikarpova, C. A. Furia, and B. Meyer, “Specifying reusable components,” in Proceedings of the 3rd International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE’10) (G. T. Leavens, P. O’Hearn, and S. Rajamani, eds.), vol. 6217 of Lecture Notes in Computer Science, pp. 127-141, Springer, August 2010.
- J. Spivey, “An introduction to Z and formal specifications,” Software Engineering Journal, 1989.
- C. A. Furia, C. M. Poskitt, and J. Tschannen, “The AutoProof verifier: Usability by non-experts and on standard code,” in Proc. Formal Integrated Development Environment (F-IDE 2015), vol. 187, pp. 42-55, Electronic Proceedings in Theoretical Computer Science (EPTCS), 2015.
- V. Rivera, S. Bhattacharya, and N. Cata˜ no, “Undertaking the tokeneer challenge in Event-B,” To appear in 4th FME Workshop on Formal Methods in Software Engineering (FormaliSE), 2016.
- J. C. M. Baeten, “A brief history of process algebra,” Theor. Comput. Sci., vol. 335, no. 2-3, pp. 131-146, 2005.
- J. Abrial, S. A. Schuman, and B. Meyer, “Specification language,” in On the Construction of Programs, pp. 343-410, 1980.
- J. Abrial, The B-book -assigning programs to meanings. Cambridge University Press, 2005.
- J.-R. Abrial, Modeling in Event-B: System and Software Engineering. New York, NY, USA: Cambridge University Press, 1st ed., 2010.
- C. B. Jones, Software Development: A Rigorous Approach. Englewood Cliffs, N.J., USA: Prentice Hall International, 1980.
- “On modelling and analysis of dynamic reconfiguration of dependable real-time systems,” in Proceedings of the 2010 Third International Conference on Dependability, DEPEND ’10, (Washington, DC, USA), pp. 173-181, IEEE Computer Society, 2010.
- M. Mazzara, “Deriving specifications of dependable systems: toward a method,” in Proceedings of the 12th European Workshop on Dependable Computing, EWDC, 2009.
- R. Gmehlich, K. Grau, A. Iliasov, M. Jackson, F. Loesch, and M. Mazzara, “Towards a formalism-based toolkit for automotive applications,” 1st FME Workshop on Formal Methods in Software Engineering (FormaliSE), 2013.
- V. Rivera, N. Cata˜ no, T. Wahls, and C. Rueda, “Code generation for Event-B.” To appear in International Journal on STTT, 2016.
- V. Rivera and N. Cata˜ no, “Translating Event-B to JML-Specified Java programs,” in 29th ACM SAC, (Gyeongju, South Korea), March 24-28 2014.
- G. T. Leavens, A. L. Baker, and C. Ruby, “Preliminary design of jml: A behavioral interface specification language for java,” SIGSOFT Softw. Eng. Notes, vol. 31, pp. 1-38, May 2006.
