基于UPPAAL的数据关联时序有限自动机模型验证

doi:10.3969/j.issn.1000-3428.2007.22.003

计算机工程 ›› 2007, Vol. 33 ›› Issue (22): 6-8,11. doi: 10.3969/j.issn.1000-3428.2007.22.003

基于UPPAAL的数据关联时序有限自动机模型验证

梁冰，刘群

（哈尔滨工程大学计算机科学技术学院，哈尔滨 150001）

收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2007-11-20 发布日期:2007-11-20

Model Verification of Data Association Temporal Finite Automata Based on UPPAAL

LIANG Bing, LIU Qun

(College of Computer Science and Technology, Harbin Engineering University, Harbin 150001)

Received:1900-01-01 Revised:1900-01-01 Online:2007-11-20 Published:2007-11-20

摘要/Abstract

摘要： 对数据关联过程建立了时序有限自动机模型，时序有限自动机时钟变量只取整数值，从而减小数据关联过程生成的状态空间。在一定的时间约束下，使用模型检测工具UPPAAL对所建模型的关键性质——关联准确性进行了分析和验证。检测结果验证了利用UPPAAL进行数据关联准确性分析的可行性。

关键词: 数据关联, 时序有限自动机, 模型检测

Abstract: A temporal finite automata model of data association(DA) using formal method is presented, and the data association process properties of accuracy are verified by the model checker UPPAAL. A practical case is also presented to justify the method using model checking UPPAAL, results show that the veracity of multi-target tracks is efficient.

Key words: data association, temporal finite automata, model check

中图分类号:

TP311

梁冰;刘群. 基于UPPAAL的数据关联时序有限自动机模型验证[J]. 计算机工程, 2007, 33(22): 6-8,11.

LIANG Bing; LIU Qun. Model Verification of Data Association Temporal Finite Automata Based on UPPAAL[J]. Computer Engineering, 2007, 33(22): 6-8,11.

http://www.ecice06.com/CN/Y2007/V33/I22/6

[1]	谢娜, 谭文安, 曹彦, 赵璐. 移动边缘计算中安全信息流建模与分析[J]. 计算机工程, 2022, 48(5): 35-42,52.
[2]	李卫超, 张铮, 王立群, 刘镇武, 刘浩. 一种拟态构造的Web威胁态势分析方法[J]. 计算机工程, 2019, 45(8): 1-6.
[3]	任胜兵,张健威,吴斌,王志健. Spark环境下基于SMT的分布式限界模型检测[J]. 计算机工程, 2017, 43(6): 19-23,29.
[4]	唐郑熠,王金水,何栋炜,薛醒思,胡文瑜. 馈线自动化算法的形式化建模与验证[J]. 计算机工程, 2016, 42(3): 89-93.
[5]	赵璐,张健沛,杨静. 收缩候选回溯集的有状态动态偏序归约方法[J]. 计算机工程, 2015, 41(5): 70-76.
[6]	许兴旺,骆翔宇. 基于MAS 模型检测与抽象的Web 服务验证[J]. 计算机工程, 2015, 41(3): 26-31,36.
[7]	劳佳琪,文中华,伍小辉,唐杰. 一种快速求强规划解的算法[J]. 计算机工程, 2015, 41(3): 162-166.
[8]	伍小辉,文中华,李洋,劳佳琪. 不确定规划中的多Agent带权值强规化算法[J]. 计算机工程, 2015, 41(1): 190-195.
[9]	龙凤,文中华,唐杰,王进宗. 不确定规划中可达关系的快速求解算法[J]. 计算机工程, 2015, 41(1): 196-199.
[10]	陆星家,郭璘,陈志荣,林勇. 基于外观和运动的车辆检测和追踪算法研究[J]. 计算机工程, 2014, 40(8): 152-157.
[11]	余莹. 组合服务交互测试研究综述[J]. 计算机工程, 2013, 39(5): 78-83.
[12]	纪明宇，王海涛，陈志远. 基于自动机的概率计算树逻辑验证方法[J]. 计算机工程, 2013, 39(12): 285-289.
[13]	徐君，张国良，敬斌，田琦. 优化的多假设FastSLAM数据关联方法[J]. 计算机工程, 2013, 39(10): 156-161.
[14]	张一弛, 庞建民, 范学斌, 姚鑫磊. 基于模型检测的程序恶意行为识别方法[J]. 计算机工程, 2012, 38(18): 107-110.
[15]	周清雷, 张兵, 席琳. 基于模型检测的系统生存性分析[J]. 计算机工程, 2012, 38(17): 38-41.

选择文件类型/文献管理软件名称

选择包含的内容

基于UPPAAL的数据关联时序有限自动机模型验证

Model Verification of Data Association Temporal Finite Automata Based on UPPAAL

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价

模态框（Modal）标题

选择文件类型/文献管理软件名称

选择包含的内容

基于UPPAAL的数据关联时序有限自动机模型验证

Model Verification of Data Association Temporal Finite Automata Based on UPPAAL

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价