Change search
ReferencesLink to record
Permanent link

Direct link
Procedure-Modular Verification of Temporal Safety Properties
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
2012 (English)Licentiate thesis, monograph (Other academic)
Abstract [en]

This thesis presents a fully automated technique for procedure-modular verification of control flow temporal safety properties. Procedure-modular verification is a natural instantiation of modular verification where modularity is achieved at the level of procedures. Here it is used for the verification of software systems 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). The technique is built on top of a previously developed modular verification framework based on maximal model construction. In the framework, program data is abstracted away completely to achieve algorithmic verification. This restricts the class of properties that can be verified. The technique is supported by a fully automated tool called ProMoVer which is described and evaluated on a number of real-life case studies. ProMoVer is quipped with a number of features, such as automatic specification extraction, to facilitate easy usage. Moreover, it provides a proof storage and reuse mechanism for efficiency.

An application area which can significantly benefit from modular verification is software product line (SPL) design. 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 a hierarchical variability model 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 hierarchical model. Therefore, scalable and efficient verification for SPL is only possible by exploiting modular verification techniques. In this thesis, we propose a hierarchical variability model for modeling product families. Then the modular verification technique and ProMoVer are adapted for the SPLs described with this hierarchical model.

A natural extension of the modular verification technique is to include program data in a conservative fashion, by encoding data from a finite domain through control. By this, a wider class of properties can be supported. As a first step towards including program data, Boolean values are added to the program model, specification languages, maximal model construction and modular verification principles.

Place, publisher, year, edition, pages
Stockholm: KTH Royal Institute of Technology, 2012. , 90 p.
Trita-CSC-A, ISSN 1653-5723
Keyword [en]
Modular Verification, Compositional Verification, Maximal Models, Model Checking, Temporal Properties
National Category
Computer Science
URN: urn:nbn:se:kth:diva-93898ISBN: 978-91-7501-337-4OAI: diva2:524550
2012-05-23, D3, Lindstedtsvägen 5, KTH, Stockholm, 13:00 (English)
QC 20120507Available from: 2012-05-03 Created: 2012-05-02 Last updated: 2012-05-07Bibliographically approved

Open Access in DiVA

fulltext(985 kB)1486 downloads
File information
File name FULLTEXT01.pdfFile size 985 kBChecksum SHA-512
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: 1486 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

Total: 352 hits
ReferencesLink to record
Permanent link

Direct link