DocumentCode
3066757
Title
Formal Verification of RGPS-S
Author
Yang, Hao ; Wu, Jinzhao
Author_Institution
Chengdu Inst. of Comput. Applic., Chinese Acad. of Sci., Chengdu, China
fYear
2011
fDate
29-31 July 2011
Firstpage
599
Lastpage
602
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/BCGIn.2011.159
Filename
6003970
Link To Document