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

作　　者：张莉[1] 杨淑贞[1] 杨浩[2] 

机构地区：[1]浙江长征职业技术学院计算机与信息技术系,浙江杭州310012 [2]浙江传媒学院新媒体学院,浙江杭州310018

出　　处：《软件导刊》2016年第12期8-10,共3页Software Guide

基　　金：浙江省教育厅一般科研项目(2016);浙江省教育中心2014年研究课题(JA049)

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

关 键 词：网络式软件 BPEL PROMELA LTL公式 正确性验证 

分 类 号：TP306[自动化与计算机技术—计算机系统结构]