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
摘要： 对数据关联过程建立了时序有限自动机模型，时序有限自动机时钟变量只取整数值，从而减小数据关联过程生成的状态空间。在一定的时间约束下，使用模型检测工具UPPAAL对所建模型的关键性质——关联准确性进行了分析和验证。检测结果验证了利用UPPAAL进行数据关联准确性分析的可行性。
关键词:
数据关联,
时序有限自动机,
模型检测
CLC Number:
LIANG Bing; LIU Qun. Model Verification of Data Association Temporal Finite Automata Based on UPPAAL[J]. Computer Engineering, 2007, 33(22): 6-8,11.
梁 冰;刘 群. 基于UPPAAL的数据关联时序有限自动机模型验证[J]. 计算机工程, 2007, 33(22): 6-8,11.