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.
展开▼
