| 基于时间扩展的ASEHA建模与验证 |
| |
| 引用本文： | 王雪红,董荣胜,余兴超. 基于时间扩展的ASEHA建模与验证[J]. 桂林电子科技大学学报, 2011, 31(2): 125-129 |
| |
| 作者姓名： | 王雪红 董荣胜 余兴超 |
| |
| 作者单位： | 桂林电子科技大学计算机科学与工程学院; |
| |
| 基金项目： | 广西自然科学基金(0991242) |
| |
| 摘 要： | 为了有效地分析实时系统,在原计算模型的基础上,引入了时钟变量,在迁移上增加了时钟约束,扩展了异步扩展层次自动机的语义.运用基于时间扩展的ASEHA,分析了ATM系统,建立了用户和ATM的模型,并使用模型检测工具UPPAAL对模型进行验证,从无死锁、活性及可达性性质出发,验证了ATM系统的安全性.实验表明,提出的基于时间...
|
| 关 键 词： | 实时系统 ASEHA 时钟约束 模型检测 UPPAAL |
Modeling and checking of ASEHA based on time extension |
| |
| Wang Xuehong,Dong Rongsheng,Yu Xingchao. Modeling and checking of ASEHA based on time extension[J]. Journal of Guilin University of Electronic Technology, 2011, 31(2): 125-129 |
| |
| Authors: | Wang Xuehong Dong Rongsheng Yu Xingchao |
| |
| Affiliation: | Wang Xuehong,Dong Rongsheng,Yu Xingchao (School of Computer Science and Engineering,Guilin University of Electronic Technology,Guilin 541004,China) |
| |
| Abstract: | In order to analyze real-time system effectively,clock variables are used and clock constraints are added in the transition based on the original model of computation.Automatic teller machine(ATM) system is analyzed and users and ATM models are built by extended ASEHA with the time.From property of no deadlock,liveness and reachability,ATM system is verified to be safe by model checking tool UPPAAL.Experiment results show that the proposed ASEHA with the time can reduce complicacy of system analysis,and hel... |
| |
| Keywords: | real-time system ASEHA clock constraints model checking UPPAAL |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
