Skip to Main content Skip to Navigation
Conference papers

Towards correct-by-construction product variants of a software product line: GFML, a formal language for feature modules

Abstract : Software Product Line Engineering (SPLE) is a software engineering paradigm that focuses on reuse and variability. Although feature-oriented programming (FOP) can implement software product line efficiently, we still need a method to generate and prove correctness of all product variants more efficiently and automatically. In this context, we propose to manipulate feature modules which contain three kinds of artifacts: specification, code and correctness proof. We depict a methodology and a platform that help the user to automatically produce correct-by-construction product variants from the related feature modules. As a first step of this project, we begin by proposing a language, GFML, allowing the developer to write such feature modules. This language is designed so that the artifacts can be easily reused and composed. GFML files contain the different artifacts mentioned above. The idea is to compile them into FoCaLiZe, a language for specification, implementation and formal proof with some object-oriented flavor. In this paper, we define and illustrate this language. We also introduce a way to compose the feature modules on some examples.
Document type :
Conference papers
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal-lirmm.ccsd.cnrs.fr/lirmm-02464897
Contributor : Nicole Levy <>
Submitted on : Monday, February 3, 2020 - 3:34:47 PM
Last modification on : Wednesday, February 5, 2020 - 1:21:48 AM
Long-term archiving on: : Monday, May 4, 2020 - 3:22:51 PM

File

PDL15.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Collections

Citation

Thi-Kim-Zung Pham, Catherine Dubois, Nicole Lévy. Towards correct-by-construction product variants of a software product line: GFML, a formal language for feature modules. 6th Workshop on Formal Methods and Analysis in SPL Engineering (FMSPLE), Apr 2015, London, United Kingdom. pp.44-55, ⟨10.4204/EPTCS.182.4⟩. ⟨lirmm-02464897⟩

Share

Metrics

Record views

74

Files downloads

155