Author(s)

Hao Yang

Corresponding Author

Hao Yang

Abstract

With the related theory and technology development of network software, network software has been widely used. Based on the characteristics of network software and framework of RGPS requirement meta-model, this paper proposes liveness verification of RGPS process layer meta-model. Firstly, it uses OWL-S language to describe RGPS process layer meta-model. Then, it uses Promela language to achieve modeling of OWL-S model. Next, it uses LTL formula to describe the properties of the Promela model and carry on liveness verification analysis of RGPS process layer meta-model. Finally, liveness verification of RGPS process layer meta-model is proved by an urban traffic system.

Keywords

OWL-S, Promela, LTL formula, Liveness verification