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.
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
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. Vol. 8997, 41 p.327-345 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8997
Keyword [en]
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: urn:nbn:se:kth:diva-128950DOI: 10.1007/978-3-319-15317-9_20Scopus ID: 2-s2.0-84922326750ISBN: 978-3-319-15316-2 (print)ISBN: 978-3-319-15317-9 (print)OAI: oai:DiVA.org:kth-128950DiVA: diva2:649033
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
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.
Series
TRITA-CSC-A, ISSN 1653-5723 ; 2014:11
National Category
Computer Science
Identifiers
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)
Opponent
Supervisors
Note

QC 20140828

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

Open Access in DiVA

fulltext(930 kB)78 downloads
File information
File name FULLTEXT07.pdfFile size 930 kBChecksum SHA-512
ca3918baeebc43d3279c4d0cf60de4a0f76a8773f59ce62991f4cddd00b1f93858ed8c008af9b73e54e4ab296fed4d193184aefb6874f42a64a94453f399e7ab
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopus

Authority records BETA

Gurov, Dilian

Search in DiVA

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

Search outside of DiVA

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

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 363 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