基于B方法的RFID中间件系统设计

摘要

随着物联网的高速发展，无线射频识别(RadioFrequencyIdentification，RFID)技术的应用范围越来越广泛，快速多样化的发展对RFID技术的适应性、灵活性及可维护性有了更高的要求，RFID中间件由此应运而生。RFID中间件能够处理来自读写器的原始标签信息，提供上层应用所感兴趣的、有效的数据，使上层应用与读写器等RFID硬件设备能够连接起来。RFID中间件从本质上来说是一个软件系统，而软件系统的缺陷和漏洞难以避免，如何保证对它的可靠性成为影响RFID系统稳定运行的关键。B方法是目前应用比较广泛的形式化方法之一，它建立在严格的数学基础之上，通过一系列的证明义务来证明系统构造的正确性，进而保证设计的正确性和系统的可靠性。
　　本文根据EPCglobal提出的RFID系统架构中对应RFID中间件的应用层事件(ApplicationLevelEvent，ALE)标准进行RFID中间件的模块划分和非形式化的设计，然后按照B方法软件开发的一般流程对系统进行设计和开发。文章首先介绍了RFID、RFID中间件和ALE标准的相关背景知识，在全面了解了B方法的数学基础、验证理论和开发过程的基础上，提炼出B方法提高软件可靠性的有利因素。然后根据应用层事件标准将RFID中间件系统划分为事件处理、访问控制和硬件管理三大模块，结合标准中相关接口的设定对RFID中间件各模块进行非形式化的设计，得到各模块的UML类图。使用B方法对模块进行形式化分析和设计，得到系统的形式化抽象模型。最后按照B方法软件开发的一般流程以事件处理模块为例，使用AtelierB工具完成抽象模型的正确性证明和自动精化，得到了模块的实现模型及自动生成的代码。

目录

声明

摘要

1 绪论

1．1 研究背景及意义

1．2 研究现状

1．3 论文的研究内容和组织结构

1．3．1 论文的研究内容

1．3．2 论文的组织结构

2 RFID及RFID中间件概述

2．1 RFID系统概述

2．1．1 RFID系统组成

2．1．2 RFID工作原理

2．2 RFID中间件

2．3 EPCglobal RFID标准

2．4 ALE

2．4．1 ALE的基本概念

2．4．2 ALE的工作模式

2．4．3 ALE的接口划分

2．5 本章小结

3 B方法的介绍

3．1 B方法基本数学知识

3．1．1 谓词和谓词逻辑

3．1．2 集合

3．2 B抽象机

3．2．1 静态行为

3．2．2 动态行为

3．3 精化／实现

3．4 B方法的证明理论

3．5 B工具

3．6 本章小结

4 RFID中间件系统的模型设计

4．1 RFID中间件的模块划分

4．2 事件处理模块的设计

4．2．1 事件处理模块的UML类图

4．2．2 事件处理模块的交互模式

4．2．3 事件处理模块的形式化设计

4．3 访问控制模块的设计

4．3．1 访问控制模块的UML类图

4．3．2 访问控制模块的形式化设计

4．4 硬件管理模块的设计

4．4．1 硬件管理模块的UML类图

4．4．2 硬件管理模块的形式化设计

4．5 本章小结

5 RFID中间件事件处理器的实现

5．1 事件处理器形式化模型的正确性证明

5．2 事件处理器形式化模型的精化与实现

5．3 本章小结

结论

致谢

参考文献

攻读学位期间的研究成果