ProMoVer: Modular Verification of Temporal Safety Properties
2011 (English)In: Software Engineering and Formal Methods (SEFM) 2011, Springer , 2011, 366-381 p.Conference paper (Refereed)
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 ofglobal properties is relativized on the local properties of the methods rather than on their implementations, and is based here on the construction of maximal models for a program model that abstracts away from program data. This approach allows global properties to be veriﬁed 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 compositionalveriﬁcation of control ﬂow safety properties, and provides appropriatepre– and post–processing. Modularity is exploited by a mechanism for proof reuse that detects and minimizes the verfication 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 methodimplementations. We evaluate the tool on a number of applications from the smart card domain.
Place, publisher, year, edition, pages
Springer , 2011. 366-381 p.
, Lecture notes in computer science, ISSN 0302-9743 ; 7041
IdentifiersURN: urn:nbn:se:kth:diva-49416DOI: 10.1007/978-3-642-24690-6ISI: 000305321300025ScopusID: 2-s2.0-81055124334ISBN: 978-3-642-24689-0OAI: oai:DiVA.org:kth-49416DiVA: diva2:459633
9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011
QC 201201112012-01-112011-11-272013-04-29Bibliographically approved