Применимость AutoProof: учебный пример верификации ПО
https://doi.org/10.15514/ISPRAS-2016-28(2)-7
Аннотация
Об авторах
Мансур Хазеев
Университет Иннополис
Россия
Россия
Виктор Ривера
Университет Иннополис
Россия
Россия
Мануэль Маццара
Университет Иннополис
Россия
Россия
Александр Чичигин
Университет Иннополис
Россия
Россия
Список литературы
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
Послать статью по эл. почте 