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

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