Abstract
Software product lines are an engineering approach to systematically build similar software products from a common asset base. When evolving such systems, it is important to have assurance that we are not introducing errors or changing the behavior of existing products. The product line refinement theory establishes the necessary conditions for such assurance. This theory has been specified and proved using the PVS proof assistant. However, the Coq proof assistant is increasingly popular among researchers and practitioners, and, given that some programming languages are already formalized into such tool, the refinement theory might benefit from the potential integration. Therefore, in this work we present a case study on porting the PVS specification of the refinement theory to Coq. We compare the proof assistants based on the noted differences between the specifications and proofs of this theory, providing some reflections on the tactics and strategies used to compose the proofs. According to our study, PVS provided more succinct definitions than Coq, in several cases, as well as a greater number of successful automatic commands that resulted in shorter proofs. Despite that, Coq also brought facilities in definitions such as enumerated and recursive types, and features that support developers in their proofs.
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
Similar content being viewed by others
Notes
- 1.
- 2.
- 3.
- 4.
- 5.
- 6.
- 7.
- 8.
References
Apel, S., Batory, D., Kästner, C., Saake, G.: Feature-Oriented Software Product Lines. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37521-7
Bodeveix, J.P., Filali, M., Munõz, C.: A formalization of the B method in Coq and PVS. In: FM’99 - B Users Group Meeting - Applying B in An Industrial Context: Tools, Lessons and Techniques, pp. 32–48. Springer, Cham (1999)
Borba, P., Teixeira, L., Gheyi, R.: A theory of software product line refinement. Theoret. Comput. Sci. 455, 2–30 (2012)
Bürdek, J., Kehrer, T., Lochau, M., Reuling, D., Kelter, U., Schürr, A.: Reasoning about product-line evolution using complex feature model differences. Autom. Softw. Eng. 23(4), 687–733 (2015). https://doi.org/10.1007/s10515-015-0185-3
Gomes, K., Teixeira, L., Alves, T., Ribeiro, M., Gheyi, R.: Characterizing safe and partially safe evolution scenarios in product lines: an empirical study. In: VaMoS. Association for Computing Machinery (2019)
Kang, K., Cohen, S., Hess, J., Novak, W., Peterson, S.: Feature-oriented domain analysis (foda) feasibility study. Technical report. CMU/SEI-90-TR-21, Software Engineering Institute, Carnegie Mellon University, November 1990
Kröher, C., Gerling, L., Schmid, K.: Identifying the intensity of variability changes in software product line evolution. In: SPLC, p. 54–64. Association for Computing Machinery (2018)
Van der Linden, F., Schmid, K., Rommes, E.: Software Product Lines in Action: the Best Industrial Practice in Product Line Engineering. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71437-8
Miller, S., Greve, D., Wilding, M., Srivas, M.: Formal verification of the Aamp-Fv microcode. Technical report (1999)
Neves, L., et al.: Safe evolution templates for software product lines. J. Syst. Softw. 106(C), 42–58 (2015)
Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference. SRI International (2001). http://pvs.csl.sri.com/doc/pvs-language-reference.pdf, version 2.4
Sampaio, G., Borba, P., Teixeira, L.: Partially safe evolution of software product lines. J. Syst. Softw. 155, 17–42 (2019)
Spadini, D., Aniche, M., Bacchelli, A.: PyDriller: Python framework for mining software repositories. In: ESEC/FSE, pp. 908–911. Association for Computing Machinery (2018)
Team, T.C.D.: The COQ proof assistant reference manual. Technical report, INRIA (2020). https://coq.inria.fr/distrib/current/refman/
Teixeira, L., Alves, V., Borba, P., Gheyi, R.: A product line of theories for reasoning about safe evolution of product lines. In: SPLC, pp. 161–170. Association for Computing Machinery (2015)
Wiedijk, F.: Comparing mathematical provers. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol. 2594, pp. 188–202. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36469-2_15
Acknowledgments
This work was partially supported by CNPq (grant 409335/2016-9) and FACEPE (APQ-0570-1.03/14), as well as INES 2.0 (http://www.ines.org.br), FACEPE grants PRONEX APQ-0388-1.03/14 and APQ-0399-1.03/17, and CNPq grant 465614/2014-0. Thayonara Alves is supported by FACEPE (grant IBPG-0749-1.03/18). Vander Alves was partially supported by CNPq (grant 310757/2018-5), FAPDF (grant SEI 00193-00000926/2019-67), and the Alexander von Humboldt Foundation.
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
Alves, T., Teixeira, L., Alves, V., Castro, T. (2020). Porting the Software Product Line Refinement Theory to the Coq Proof Assistant. In: Carvalho, G., Stolz, V. (eds) Formal Methods: Foundations and Applications. SBMF 2020. Lecture Notes in Computer Science(), vol 12475. Springer, Cham. https://doi.org/10.1007/978-3-030-63882-5_12
Download citation
DOI: https://doi.org/10.1007/978-3-030-63882-5_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-63881-8
Online ISBN: 978-3-030-63882-5
eBook Packages: Computer ScienceComputer Science (R0)