Change search
ReferencesLink to record
Permanent link

Direct link
Procedure-Modular Specification and Verification of Temporal Safety Properties
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
University of Twente.
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 [en]
Temporal logic, Model checking, Maximal models
National Category
Computer Science
URN: urn:nbn:se:kth:diva-129204DOI: 10.1007/s10270-013-0321-0ISI: 000349026100007ScopusID: 2-s2.0-84922337820OAI: diva2:650753
Swedish Research Council

QC 20130926

Available from: 2013-09-23 Created: 2013-09-23 Last updated: 2015-03-25Bibliographically 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

man.pdf(557 kB)74 downloads
File information
File name FULLTEXT01.pdfFile size 557 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopusThe final publication is available at

Search in DiVA

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

Search outside of DiVA

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

Altmetric score

Total: 76 hits
ReferencesLink to record
Permanent link

Direct link