NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
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
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)
Date Acquired
August 25, 2013
Publication Date
August 1, 2011
Subject Category
Numerical Analysis
Report/Patent Number
NF1676L-13249
NASA/CR-2011-217170
Funding Number(s)
CONTRACT_GRANT: CMU-PT/SE/0038/2008
CONTRACT_GRANT: NNX08AC59A
WBS: WBS 534723.02.02.07.40
Distribution Limits
Public
Copyright
Public Use Permitted.

Available Downloads

NameType 20110014510.pdf STI