Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 14 / Issue 12

available in:   PDF (163 kB) PS (183 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-014-12-2059


Modularizing Theorems for Software Product Lines: The Jbook Case Study

Don Batory (University of Texas at Austin, USA)

Egon Börger (Università di Pisa, Italy)

Abstract: A goal of software product lines is the economical assembly of programs in a family of programs. In this paper, we explore how theorems about program properties may be integrated into feature-based development of software product lines. As a case study, we analyze an existing Java/JVM compilation correctness proof for defining, interpreting, compiling, and executing bytecode for the Java language. We show how features modularize program source, theorem statements and their proofs. By composing features, the source code, theorem statements and proofs for a program are assembled. The investigation in this paper reveals a striking similarity of the refinement concepts used in Abstract State Machines (ASM) based system development and Feature-Oriented Programming (FOP) of software product lines. We suggest to exploit this observation for a fruitful interaction of researchers in the two communities.

Keywords: AHEAD, ASM, composition, features, verification

Categories: D.2.1, D.2.10, D.2.11, D.2.4