Preview

Труды Института системного программирования РАН

Расширенный поиск

Применимость AutoProof: учебный пример верификации ПО

https://doi.org/10.15514/ISPRAS-2016-28(2)-7

Полный текст:

Аннотация

Очень часто инструменты статической верификации являются результатом многолетних научно-исследовательских работ. По этой причине разработки ведутся с распределением задач внутри учебных заведений и с расчетом на способность старших исследователей обеспечивать её непрерывность. В такой ситуации некоторые атрибуты качества, такие как удобство и простота использования программного обеспечения, чаще всего, не рассматриваются на должном уровне, что плохо сказывается на возможности дальнейшей коммерциализации продукта. Для того, чтобы данные инструменты получили широкое применение необходимо обратить внимание и направить усилия при дальнейшей доработке на упрощение механизма взаимодействия пользователей с приложением, для того, чтобы дать инженерам программного обеспечения возможность пользоваться инструментом без необходимости полного понимания всех математических механизмов во всех деталях. Для того, чтобы обратить внимание общественности на важность удобства использования инструментов верификации, мы применили инструмент AutoProof к хорошо известному проекту Tokeneer. Данный инструмент использовался для верификации части имплементации реального проекта Tokeneer, в ходе чего были выявлены сильные и слабые стороны AutoProof, и, как результат, был составлен список необходимых улучшений. Результат данной работы иллюстрирует эффективность инструмента при верификации фрагмента реального программного обеспечения: он позволил автоматически проверить практически две трети всех свойств. В то же время, данное исследование показало потребность в доработке документации к данному инструменту и подчеркнуло необходимость улучшения как самого инструмента, так и среды Eiffel IDE.

Об авторах

Мансур Хазеев
Университет Иннополис
Россия


Виктор Ривера
Университет Иннополис
Россия


Мануэль Маццара
Университет Иннополис
Россия


Александр Чичигин
Университет Иннополис
Россия


Список литературы

1. B. Meyer, Touch of Class: Learning to Program Well with Objects and Contracts. Springer Publishing Company, Incorporated, 1 ed., 2009.

2. 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.

3. E. M. Clarke, Jr., O. Grumberg, and D. A. Peled, Model Checking. Cambridge, MA, USA: MIT Press, 1999.

4. 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.

5. 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.

6. B. Meyer, Object-oriented software construction, ch. 11: Design by Contract: building reliable software. Prentice Hall PTR, 1997.

7. AdaCore, “Tokeneer.” http://www.adacore.com/sparkpro/tokeneer/download, accessed in April 2016.

8. 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.

9. J. Barnes, High Integrity Software: The SPARK Approach to Safety and Security. Boston, MA, USA: Addison-Wesley Longman Publishing Co., Inc., 2003.

10. K. R. M. Leino, “This is boogie 2,” tech. rep., June 2008.

11. 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.

12. J. Spivey, “An introduction to Z and formal specifications,” Software Engineering Journal, 1989.

13. 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.

14. 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.

15. J. C. M. Baeten, “A brief history of process algebra,” Theor. Comput. Sci., vol. 335, no. 2-3, pp. 131–146, 2005.

16. J. Abrial, S. A. Schuman, and B. Meyer, “Specification language,” in On the Construction of Programs, pp. 343–410, 1980.

17. J. Abrial, The B-book - assigning programs to meanings. Cambridge University Press, 2005.

18. J.-R. Abrial, Modeling in Event-B: System and Software Engineering. New York, NY, USA: Cambridge University Press, 1st ed., 2010.

19. C. B. Jones, Software Development: A Rigorous Approach. Englewood Cliffs, N.J., USA: Prentice Hall International, 1980.

20. “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.

21. M. Mazzara, “Deriving specifications of dependable systems: toward a method,” in Proceedings of the 12th European Workshop on Dependable Computing, EWDC, 2009.

22. 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.

23. V. Rivera, N. Cata˜ no, T. Wahls, and C. Rueda, “Code generation for Event-B.” To appear in International Journal on STTT, 2016.

24. 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.

25. 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.


Для цитирования:


Хазеев М., Ривера В., Маццара М., Чичигин А. Применимость AutoProof: учебный пример верификации ПО. Труды Института системного программирования РАН. 2016;28(2):111-126. https://doi.org/10.15514/ISPRAS-2016-28(2)-7

For citation:


Khazeev M., Rivera V., Mazzara M., Tchitchigin A. Usability of AutoProof: a case study of software verification. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2016;28(2):111-126. https://doi.org/10.15514/ISPRAS-2016-28(2)-7

Просмотров: 116


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


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