Change search
ReferencesLink to record
Permanent link

Direct link
Model Mining and Efficient Verification of Software Product Lines
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
Norwegian Computing Center, Oslo.
University of Sofia, Sofia.
(English)Manuscript (preprint) (Other academic)
National Category
Computer Science
URN: urn:nbn:se:kth:diva-149880OAI: diva2:741447

QS 2014

Available from: 2014-08-28 Created: 2014-08-28 Last updated: 2014-08-28Bibliographically approved
In thesis
1. Algorithmic Verification of Procedural Programs in the Presence of Code Variability
Open this publication in new window or tab >>Algorithmic Verification of Procedural Programs in the Presence of Code Variability
2014 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

This thesis addresses the formal verification of temporal properties of procedural programs that are dynamically or statically configured by replacing, adapting, or adding new components. Dealing with such variable programs is challenging because a part of the program is either not available at verification time or changes frequently. Still, such static and dynamic variability is used in a variety of modern software systems and design paradigms, e.g., software product lines. In this thesis, we develop a generic framework and a fully automated tool support for the verification of such programs. We also show that our technique can be used for efficient verification of existing sets of products constructed from product lines. Our framework is built on top of a previously developed framework for compositional verification of control-flow safety properties of procedural programs that abstracts away all program data. The work in this study is presented through three papers.

The first paper introduces ProMoVer, a fully automated tool for procedure modular verification of control-flow temporal safety properties. Procedure modular verification is a natural instantiation of compositional verification at the procedure level. ProMoVer is described and evaluated on several real-life case studies. It is equipped with a number of features, such as automatic specification extraction and the support for several specification formalisms, to facilitate easy usage. Moreover, it provides a proof storage and reuse mechanism to minimize the need for the computationally expensive verification subtasks.

The second paper discusses the verification of software product lines (SPL). In SPL engineering, products are generated from a set of well-defined commonalities and variabilities. The products of an SPL can be described by means of hierarchical variability models specifying the commonalities and variabilities between the individual products. The number of products generated from a hierarchical model is exponential in the size of the model. Therefore, scalable verification of SPLs is only possible if compositional techniques are applied that allow reusing of the intermediate verification results. In this thesis, we propose a hierarchical variability model for modeling product families, provide a process for extracting such models from existing products, and adapt our compositional verification principle and tool support for the verification of SPLs modeled by this hierarchical model.

The third paper presents a generalization of the original framework to capture program data, still keeping its complexity within practical limits. Thus, it brings the capabilities of the framework to a whole new level. To exemplify its use, we instantiate our framework for compositional verification at three levels of data abstraction of real-life programs: full data abstraction, Boolean data as the only datatype, and heap pointers as the only datatype. We also adapt our toolset to provide support for compositional verification of the latter and evaluate the tool on a real-life case study.

Place, publisher, year, edition, pages
Stockholm: KTH Royal Institute of Technology, 2014. vii, 67 p.
TRITA-CSC-A, ISSN 1653-5723 ; 2014:11
National Category
Computer Science
urn:nbn:se:kth:diva-149735 (URN)978-91-7595-211-6 (ISBN)
Public defence
2014-09-19, F3, Lindstedtsvägen 26 Kungl Tekniska högskolan, Stockholm, 14:00 (English)

QC 20140828

Available from: 2014-08-28 Created: 2014-08-26 Last updated: 2014-08-29Bibliographically approved

Open Access in DiVA

No full text

Search in DiVA

By author/editor
Soleimanifard, SiavashGurov, Dilian
By organisation
Theoretical Computer Science, TCS
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 128 hits
ReferencesLink to record
Permanent link

Direct link