RGPS服务层元模型正确性验证

随着网络式软件复杂程度的日益增加，如何确保网络式软件功能和性能的正确性越发重要。根据网络式软件的特点，在RGPS需求元建模框架的指导下，提出RGPS服务层元模型正确性验证。首先用BPEL语言和WSDL语言把RGPS服务层元模型描述成BPEL模型，再用Promela语言实现BPEL模型的建模，最后输入LTL公式对RGPS服务层元模型进行安全性和活性验证分析。以城市交通出行系统为例，采用RGPS需求元模型为框架，构建城市交通出行系统服务层元模型。