Automated Verification of Specifications with Typestates and Access Permissions - Siminiceanu, Radu; Ahmed, Ijaz; Catano, Nestor (Electronic Communications of the EASST, 2012)
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.