-
题名基于时间扩展的ASEHA建模与验证
- 1
-
-
作者
王雪红
董荣胜
余兴超
-
机构
桂林电子科技大学计算机科学与工程学院
-
出处
《桂林电子科技大学学报》
2011年第2期125-129,共5页
-
基金
广西自然科学基金(0991242)
-
文摘
为了有效地分析实时系统,在原计算模型的基础上,引入了时钟变量,在迁移上增加了时钟约束,扩展了异步扩展层次自动机的语义。运用基于时间扩展的ASEHA,分析了ATM系统,建立了用户和ATM的模型,并使用模型检测工具UPPAAL对模型进行验证,从无死锁、活性及可达性性质出发,验证了ATM系统的安全性。实验表明,提出的基于时间扩展的ASEHA能够降低系统分析的复杂性,有助于实时系统的建模与验证。
-
关键词
实时系统
aseha
时钟约束
模型检测
UPPAAL
-
Keywords
real-time system
aseha
clock constraints
model checking
UPPAAL
-
分类号
TP301.1
[自动化与计算机技术—计算机系统结构]
-
-
题名基于时间扩展的Web服务模型检测
- 2
-
-
作者
王雪红
刘柯威
陈冠萍
胡元闯
-
机构
贺州学院计算机科学与信息工程学院
-
出处
《佛山科学技术学院学报（自然科学版）》
CAS
2017年第2期14-17,共4页
-
基金
广西自然科学基金资助项目(2014jj BA70066)
贺州学院校级科研项目(2014ZC22)
+1 种基金
贺州学院校级教改项目(hzxyjg201514
hzxyjg201515)
-
文摘
由于传统的形式化方法不能保证带时间约束的组合Web服务安全可靠地运行,为了有效地分析并确保带时间约束的组合Web服务的正确性,利用时间自动机验证工具UPPAAL将带时间约束的组合Web服务的每个原子服务建立自动机模型,给出ASEHA语义描述,并用模拟器模拟带时间约束的Web服务的运行过程,对带有时间约束的Web服务的属性进行分析。最后,以旅行预订票组合系统为例,验证其死锁、活性和安全性。实例证明此方法有效。
-
关键词
WEB服务
aseha
时钟约束
UPPAAL
-
Keywords
Web services
aseha
clock constraints
UPPAAL
-
分类号
TP393.09
[自动化与计算机技术—计算机应用技术]
-
-
题名组合Web服务的建模与BPEL语言描述
被引量：1
- 3
-
-
作者
王雪红
刘柯威
-
机构
贺州学院计算机科学与信息工程学院
武汉大学计算机学院
-
出处
《计算机光盘软件与应用》
2014年第7期141-142,共2页
-
基金
广西高等学校立项科研项目(项目编号:201204LX461)
贺州学院校级科研项目(项目编号:2012ZRKY07)
贺州学院校级科研项目(项目编号:2012ZRKY06)资助
-
文摘
基于时间扩展的ASEHA自动机理论,以旅行预订票组合Web服务为例,分别建立了旅行者(Traveler)、旅行代理(Travel Agent)及航空公司预订票(Airline Reservation)三个自动机,并给出该服务的BPEL语言描述。
-
关键词
组合WEB服务
aseha
BPEL
-
分类号
TP301.1
[自动化与计算机技术—计算机系统结构]
-
