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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)
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)
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-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.2408795
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)
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)
ETH Zurich.: AutoProof tutorial - chair of software engineering. http://se.inf.ethz.ch/research/autoproof/tutorial
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.4
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.1592439
McConnell, S.: Managing technical debt. Technical report, Construx Software (2008)
Meyer, B.: On formalism in specifications. IEEE Softw. 2(1), 6–26 (1985). https://doi.org/10.1109/MS.1985.229776
Meyer, B.: Applying “design by contract”. Computer 25(10), 40–51 (1992)
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)
Polikarpova, N.: Specified and verified reusable components (2014). https://doi.org/10.3929/ethz-a-010163357
Pressman, R.S.: Software Engineering: A Practitioner’s Approach, 7th edn. McGraw-Hill Higher Education, New York (2010). OCLC: ocn271105592
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)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Khazeev, M., Mazzara, M., Aslam, H., de Carvalho, D. (2020). Towards a Broader Acceptance of Formal Verification Tools. In: Auer, M., Hortsch, H., Sethakul, P. (eds) The Impact of the 4th Industrial Revolution on Engineering Education. ICL 2019. Advances in Intelligent Systems and Computing, vol 1135. Springer, Cham. https://doi.org/10.1007/978-3-030-40271-6_20
Download citation
DOI: https://doi.org/10.1007/978-3-030-40271-6_20
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-40270-9
Online ISBN: 978-3-030-40271-6
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)