Title :
Formal Verification of RGPS-S
Author :
Yang, Hao ; Wu, Jinzhao
Author_Institution :
Chengdu Inst. of Comput. Applic., Chinese Acad. of Sci., Chengdu, China
Abstract :
Based on the basic concept of the service layer of the requirement meta-modeling frame for network software (RGPS-S), this paper proposed a new formal method to verify its correctness. This paper gives the transform method from BPEL model to Promela model and verifies the model based on SPIN. At last, we performed an exhaustive verification run with SPIN to demonstrate some basic safety properties and liveness properties.
Keywords :
business process re-engineering; formal verification; meta data; service-oriented architecture; BPEL model; Promela model; RGPS-S; SPIN; formal verification; network software; requirement meta-modeling frame; service layer; Business; Computational modeling; Formal verification; Medical services; Metamodeling; Safety; Software; BPEL; Promela; RGPS-S; SPIN; formal method;
Conference_Titel :
Business Computing and Global Informatization (BCGIN), 2011 International Conference on
Conference_Location :
Shanghai
Print_ISBN :
978-1-4577-0788-9
Electronic_ISBN :
978-0-7695-4464-9
DOI :
10.1109/BCGIn.2011.159
