국내 최대 기계 및 로봇 연구정보

기술보고서

기술보고서 게시판 내용
타이틀	Automated Verification of Specifications with Typestates and Access Permissions
저자	Siminiceanu, Radu I.;; Catano, Nestor
Keyword	ALGORITHMS;; APPROACH CONTROL;; CONSTRUCTION;; DATA FLOW ANALYSIS;; EXHAUSTING;; PARALLEL PROGRAMMING;; PROGRAM VERIFICATION (COMPUTERS); SPECIFICATIONS
URL	http://hdl.handle.net/2060/20110014510
보고서번호	NASA/CR-2011-217170
발행년도	2011
출처	NTRS (NASA Technical Report Server)
ABSTRACT	We 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).