-
题名RGPS过程层元模型正确性验证
被引量:1
- 1
-
-
作者
袁开银
郭瑞
陆翔升
吴尽昭
-
机构
河南财经政法大学现代教育技术中心
郑州轻工业学院计算机与通信工程学院
中国科学院成都计算机应用研究所
-
出处
《计算机工程》
CAS
CSCD
2012年第15期39-42,共4页
-
基金
国家"863"计划基金资助项目"基于代数符号计算的新型软件形式化验证技术和支持工具"(2007AA01Z143)
-
文摘
利用Web服务本体描述语言对RGPS过程层元模型进行描述,建立Promela模型。基于线性时序逻辑,以及Spin检测工具的偏序规约和on-the-fly等优化技术对Promela模型进行正确性验证,设计并实现RGPS过程层元模型正确性验证平台。通过城市交通系统实例证明该验证方法的正确性和有效性。
-
关键词
RGPS框架
promela建模
Spin模型检测工具
过程层元模型
线性时序逻辑
-
Keywords
Role Goal Process Service(RGPS) framework
promela modeling
Spin model checking tool
process level meta-model
Linear Temporal Logic(LTL)
-
分类号
TP393.07
[自动化与计算机技术—计算机应用技术]
-
-
题名基于SPIN的功能测试用例生成方法研究
- 2
-
-
作者
李建
杨晋吉
-
机构
华南师范大学计算机学院
-
出处
《软件导刊》
2016年第7期1-4,共4页
-
基金
国家自然科学基金项目(61272066)
-
文摘
提出了一种自动生成系统功能测试用例的新方法。该方法使用Promela语言对软件系统的状态和行为进行描述建模,使用LTL公式描述测试覆盖标准,然后将该组LTL公式和描述状态行为的Promela模型输入SPIN模型检测工具,并利用模型检测工具自动生成相应的证据路径,最后结合正例将路径转化成满足相应覆盖标准的系统功能测试用例,并以电梯系统模型对该方法作出了诠释。
-
关键词
功能测试用例
SPIN
模型检测
promela建模
-
分类号
TP306
[自动化与计算机技术—计算机系统结构]
-