Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Algorithmic Verification of Procedural Programs in the Presence of Code Variability
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
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.
Series
TRITA-CSC-A, ISSN 1653-5723 ; 2014:11
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-149735ISBN: 978-91-7595-211-6 (print)OAI: oai:DiVA.org:kth-149735DiVA: diva2:740903
Public defence
2014-09-19, F3, Lindstedtsvägen 26 Kungl Tekniska högskolan, Stockholm, 14:00 (English)
Opponent
Supervisors
Note

QC 20140828

Available from: 2014-08-28 Created: 2014-08-26 Last updated: 2014-08-29Bibliographically approved
List of papers
1. Procedure-Modular Specification and Verification of Temporal Safety Properties
Open this publication in new window or tab >>Procedure-Modular Specification and Verification of Temporal Safety Properties
2013 (English)In: Software & Systems Modeling, ISSN 1619-1366Article in journal (Refereed) Published
Abstract [en]

This paper describes ProMoVer, a tool for fully automated procedure-modular verification of Java programs equipped with method-local and global assertions that specify safety properties of sequences of method invocations. Modularity at the procedure-level is a natural instantiation of the modular verification paradigm, where correctness of global properties is relativized on the local properties of the methods rather than on their implementations. Here, it is based on the construction of maximal models for a program model that abstracts away from program data. This approach allows global properties to be verified in the presence of code evolution, multiple method implementations (as arising from software product lines), or even unknown method implementations (as in mobile code for open platforms). ProMoVer automates a typical verification scenario for a previously developed tool set for compositional verification of control flow safety properties, and provides appropriate pre- and post-processing. Both linear-time temporal logic and finite automata are supported as formalisms for expressing local and global safety properties, allowing the user to choose a suitable format for the property at hand. Modularity is exploited by a mechanism for proof reuse that detects and minimizes the verification tasks resulting from changes in the code and the specifications. The verification task is relatively light-weight due to support for abstraction from private methods and automatic extraction of candidate specifications from method implementations. We evaluate the tool on a number of applications from the domains of Java Card and web-based application.

Place, publisher, year, edition, pages
Springer, 2013
Keyword
Temporal logic, Model checking, Maximal models
National Category
Computer Science
Identifiers
urn:nbn:se:kth:diva-129204 (URN)10.1007/s10270-013-0321-0 (DOI)000349026100007 ()2-s2.0-84922337820 (Scopus ID)
Funder
Swedish Research Council
Note

QC 20130926

Available from: 2013-09-23 Created: 2013-09-23 Last updated: 2015-03-25Bibliographically approved
2. Model Mining and Efficient Verification of Software Product Lines
Open this publication in new window or tab >>Model Mining and Efficient Verification of Software Product Lines
(English)Manuscript (preprint) (Other academic)
National Category
Computer Science
Identifiers
urn:nbn:se:kth:diva-149880 (URN)
Note

QS 2014

Available from: 2014-08-28 Created: 2014-08-28 Last updated: 2014-08-28Bibliographically approved
3. 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
2015 (English)In: Formal Aspects of Component Software: 11th International Symposium, FACS 2014, Bertinoro, Italy, September 10-12, 2014, Revised Selected Papers, Springer, 2015, Vol. 8997, 41 p.327-345 p.Conference paper, Published paper (Refereed)
Abstract [en]

We present a generic framework for verifying temporal safety properties of procedural programs that are dynamically or statically configured by replacing, adapting, or adding new components. To deal with such a variability of a program, we require programmers to provide local specifications for its variable components, and verify the global properties by replacing these specifications with maximal models. Our framework is a generalization of a previously developed framework that abstracts from all program data. In this work, we capture program data and thus significantly increase the range of properties that can be verified. Our framework is generic by being parametric on the set of observed program events and their semantics. We separate program structure from the behavior it induces to facilitate independent component specification and verification. We provide tool support for an instantiation of our framework to programs written in a procedural language with pointers as the only datatype.

Place, publisher, year, edition, pages
Springer, 2015. 41 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8997
Keyword
Algorithms, Computer software, Semantics, Algorithmic verification, Generic frameworks, Global properties, Independent components, New components, Procedural languages, Program structures, Temporal safety properties
National Category
Computer Science
Identifiers
urn:nbn:se:kth:diva-128950 (URN)10.1007/978-3-319-15317-9_20 (DOI)2-s2.0-84922326750 (Scopus ID)978-3-319-15316-2 (ISBN)978-3-319-15317-9 (ISBN)
Conference
11th International Symposium on Formal Aspects of Component Software, FACS 2014, Bertinoro, Italy, 10 September 2014 through 12 September 2014
Note

QC 20150504. Updated from manuscript to conference paper.

Available from: 2013-09-17 Created: 2013-09-17 Last updated: 2015-05-04Bibliographically approved

Open Access in DiVA

Thesis(2212 kB)414 downloads
File information
File name FULLTEXT04.pdfFile size 2212 kBChecksum SHA-512
f296b0abec4fe034d76573861c98d1f62a01929e76bf64c0b93097df3966bad34872f364c16db51c9e75715e76f5185e86341c4758b31bcd8c0dface00b2713b
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Soleimanifard, Siavash
By organisation
Theoretical Computer Science, TCS
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 415 downloads
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

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 734 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf