论文部分内容阅读
随着网络技术的不断发展,物联网/物理信息融合系统成为目前研究和发展的热点。一个典型的例子是智能交通系统(ITS)。通信作为信息交换的媒介,已成为物联网研究的核心问题之一。在智能交通系统中,车辆可以与服务中心沟通(V2I),告知其他车辆他们的存在以便于车辆的安全监控和安全驾驶;另外车辆和车辆之间也可以通信(V2V),从而提高交通的安全性,避免恶性交通事故的发生。该系统通信的实时性研究是非常重要的。分布式的系统通信更强调逻辑时钟。为此本论文提出一种新型的适用于分布式系统通信的时间化网络通信模型(Timed-pNets)。该模型包括了刻画时间化动作(Time Action)的逻辑时钟(Logical Clock)、时间化规范(Timed Specification)、时间参数化标签迁移系统(timed Parameterized Label Transition System,timed-pLTS)等基本构件。Timed-pNets是树型分层结构模型,其叶子节点由Timed-pLTS表述,非叶子节点是子网的抽象,用于同步子网之间的通信。本论文的主要贡献如下:·建立了一个分布式具有同步和异步通信的时间化模型Timed-pNets。在引入时间化动作形成动作逻辑时钟基础上,建立时间化的pLTS系统(Timed-pLTS)。Timed-pLTS中的标签为逻辑时钟,用于触发系统从一个状态迁移到另一个状态。论文把信道设计为Timed-pLTS,具有信息接受和发送两个动作逻辑时钟,用来描述异步通信。基于Timed-pLTS,论文构造了Timed-pNets模型,它的同步向量用于描述不同节点之间的同步通信。研究Timed-pNets的相容性(Compatibility)和延迟性(Delay)。·提出了时间规范(Timed Specication)的概念。时间规范定义为一组逻辑时钟和这些时钟上的关系,包括时钟优先关系和时钟同步关系。提出了时钟划分和时钟合并的概念以简化时间规范,研究了时钟的优先关系和同步关系作用在划分后时钟上的语义。·设计了一组算法用于把Timed-pLTS和Timed-pNets转化为时间规范,并提出了一套利用时间规范来建立层次化模型的理论和方法。这样人们可以灵活地设计通信系统:既可以先设计叶子节点,然后组合成Timed-pNets节点这种层层向上的方法构建系统,也可以先设计一个抽象的Timed-pNets系统,然后用具体的Timed-pLTS实例化该系统中每个抽象孔的由上至下方式构建系统。●以智能交通系统中车辆相互通信为例子,实现如何建立Timed-pNets模型,以及检查通信的安全性和时间性质。使用TimeSquare工具完成这些性质的测试,结果表明论文建立的timed-pNets具有通用性和灵活性。