Advertisement

Towards a Broader Acceptance of Formal Verification Tools

The Role of Education
  • Mansur KhazeevEmail author
  • Manuel Mazzara
  • Hamna Aslam
  • Daniel de Carvalho
Conference paper
  • 17 Downloads
Part of the Advances in Intelligent Systems and Computing book series (AISC, volume 1135)

Abstract

Formal methods face challenges towards wide acceptance and adoption in software development practices. The major reason is presumed complexity of the concepts, tools and formal processes. The issue can be addressed by academia with a thoughtful plan of teaching and practise. The user study detailed in this paper is examining AutoProof tool with the motivation to identify complexities attributed to formal methods. Participants’ (students of Masters program in Computer Science) performance and feedback on the experience with formal methods assisted us in extracting specific problem areas that effect tool usability. The study results infer, along with improvements in verification tool functionalities, that teaching programs need to be modified by including pre-requisite courses to make formal methods easily adapted by students and promote their usage in software development process.

References

  1. 1.
    Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)CrossRefGoogle Scholar
  2. 2.
    Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.L., Muntean, T. (eds.) Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, pp. 49–69. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  3. 3.
    Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. 7(3), 212–232 (2005).  https://doi.org/10.1007/s10009-004-0167-4CrossRefGoogle Scholar
  4. 4.
    Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. ACM 56(2), 82–90 (2013).  https://doi.org/10.1145/2408776.2408795CrossRefGoogle Scholar
  5. 5.
    de Carvalho, D., Hussain, R., Khan, A., Khazeev, M., Lee, J., Masiagin, S., Mazzara, M., Mustafin, R., Naumchev, A., Rivera, V.: Teaching programming and design-by-contract. Advances in Intelligent Systems and Computing, pp. 68–76 (2020)Google Scholar
  6. 6.
    Dougiamas, M., Taylor, P.C.: Moodle: using learning communities to create an open source course management system. In: Proceedings of the EDMEDIA 2003 Conference, Honolulu, Hawaii (2003)Google Scholar
  7. 7.
    ETH Zurich.: AutoProof tutorial - chair of software engineering. http://se.inf.ethz.ch/research/autoproof/tutorial
  8. 8.
    Furia, C.A., Poskitt, C.M., Tschannen, J.: The autoproof verifier: usability by non-experts and on standard code. In: Proceedings Formal Integrated Development Environment (F-IDE 2015), Electronic Proceedings in Theoretical Computer Science, vol. 187, pp. 42–55 (2015).  https://doi.org/10.4204/EPTCS.187.4CrossRefGoogle Scholar
  9. 9.
    Hoare, C., Misra, J., Leavens, G.T., Shankar, N.: The verified software initiative: a manifesto. ACM Comput. Surv. 41(4), 22:1–22:8 (2009).  https://doi.org/10.1145/1592434.1592439CrossRefGoogle Scholar
  10. 10.
    McConnell, S.: Managing technical debt. Technical report, Construx Software (2008)Google Scholar
  11. 11.
    Meyer, B.: On formalism in specifications. IEEE Softw. 2(1), 6–26 (1985).  https://doi.org/10.1109/MS.1985.229776CrossRefGoogle Scholar
  12. 12.
    Meyer, B.: Applying “design by contract”. Computer 25(10), 40–51 (1992)CrossRefGoogle Scholar
  13. 13.
    Neumann, R.: Using promela in a fully verified executable LTL model checker. In: Giannakopoulou, D., Kroening, D. (eds.) Verified Software: Theories, Tools and Experiments, pp. 105–114. Springer, Cham (2014)Google Scholar
  14. 14.
    Polikarpova, N.: Specified and verified reusable components (2014).  https://doi.org/10.3929/ethz-a-010163357
  15. 15.
    Pressman, R.S.: Software Engineering: A Practitioner’s Approach, 7th edn. McGraw-Hill Higher Education, New York (2010). OCLC: ocn271105592zbMATHGoogle Scholar
  16. 16.
    Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N.: Autoproof: auto-active functional verification of object-oriented programs. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 566–580. Springer, Heidelberg (2015)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  • Mansur Khazeev
    • 1
    Email author
  • Manuel Mazzara
    • 1
  • Hamna Aslam
    • 1
  • Daniel de Carvalho
    • 1
  1. 1.Innopolis UniversityInnopolisRussia

Personalised recommendations