Automated Verification of Specifications with Typestates and Access PermissionsWe propose an approach to formally verify Plural specifications based on access permissions and typestates, by model-checking automatically generated abstract state-machines. Our exhaustive approach captures all the possible behaviors of abstract concurrent programs implementing the specification. We describe the formal methodology employed by our technique and provide an example as proof of concept for the state-machine construction rules. The implementation of a fully automated algorithm to generate and verify models, currently underway, provides model checking support for the Plural tool, which currently supports only program verification via data flow analysis (DFA).
Document ID
20110014510
Acquisition Source
Langley Research Center
Document Type
Contractor Report (CR)
Authors
Siminiceanu, Radu I. (National Inst. of Aerospace Hampton, VA, United States)
Catano, Nestor (Madeira ITI Campus da Penteada, Funchal, Portugal)