Specification and Verification of Policy Using RAISE and ModelChecking
In order to understand and describe the domain of system applications, and provide a good formal basis for requirements engineering, this paper takes policy as research object of domain engineering, and proposes a method of specification and verification of policy. Firstly, we construct policy model in which the entity, function, event and action in policy are specified with RAISE Specification Language, and the properties of policy are specified with LTL formula. Secondly, we translate RSL specifications automatically into the input language PROMELA of the SPIN model checker for verifying the correctness of the policy model. For this purpose, we define a syntactic translation between RSL and PROMELA, and show the correctness of the translation. Finally, we give a case study which automatically translates the RSL specifications of the policy of social insurance into PROMELA, and verifies the correctness of policy model with SPIN.
RSL PROMELA SPIN Model checking policy verification
Tao Zhang Shaobin Huang Tianyang Lv Hongtao Huang
College of Computer Science and Technology Harbin Engineering University Harbin, Heilongjiang Province, China, 150001
国际会议
上海
英文
2095-2099
2011-10-15（万方平台首次上网日期，不代表论文的发表时间）