文章基本信息

标题：Automated Verification of Specifications with Typestates and Access Permissions
本地全文：下载
作者：Radu I. Siminiceanu ; Ijaz Ahmed ; Nestor Catano 等
期刊名称：Electronic Communications of the EASST
电子版ISSN：1863-2122
出版年度：2012
卷号：53
语种：English
出版社：European Association of Software Science and Technology (EASST)
摘要：We propose an approach to formally verify Plural specifications of concurrent programs based on access permissions and typestates, by model-checking automatically generated abstract state-machines. Our approach captures all possible relevant behaviors of abstract concurrent programs implementing the specification. We describe the formal methodology employed in our technique and provide an example as proof of concept for the state-machine construction rules. We implemented the fully automated algorithm to generate and verify models as a freely available plug-in of the Plural tool, called Pulse. We tested Pulse on the full specification of a Multi Threaded Task Server commercial application and showed that this approach scales well and is efficient in finding errors in specifications that could not be previously detected with the Data Flow Analysis (DFA) capabilities of Plural.