Verifying the IEEE 1394 FireWire Tree Identify Protocol with SMV

This case study contains a formal verification of the IEEE 1394 FireWire tree identify protocol. Crucial properties of finite models of the protocol have been validated with state-of-the-art symbolic model checkers. Various optimisation techniques were applied to verify concrete and generic configurations. Received September 2001/Accepted in revised form September 2001 Correspondence and offprint requests to: Viktor Schuppan, Computer Systems Institute, ETH Zurich, 8092 Zurich, Switzerland. Email: Viktor.Schuppan@inf.ethz.ch     

Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394

The IEEE 1394 high performance serial multimedia bus protocol allows several components to communicate with each other at high speed. In this paper we present a formal model and verification of a leader election algorithm that forms the core of the tree identify phase of the physical layer of the 1394 protocol.We describe the algorithm formally in the I/O automata model of Lynch and Tuttle, and verify that for an arbitrary tree topology exactly one leader is elected. A large part of our verification has been checked mechanically with PVS, a verification system for higher-order logic.     

Automatic Verification of the IEEE-1394 Root Contention Protocol with KRONOS and PRISM

We report on the automatic verification of timed probabilistic properties of the IEEE 1394 root contention protocol combining two existing tools: the real-time model-checker KRONOS and the probabilistic model-checker PRISM. The system is modelled as a probabilistic timed automaton. We first use KRONOS to perform a symbolic forward reachability analysis to generate the set of states that are reachable with non-zero probability from the initial state, and before the deadline expires. We then encode this information as a Markov decision process to be analyzed with PRISM. We apply this technique to compute the minimal probability of a leader being elected before a deadline, for different deadlines, and study the influence of using a biased coin on this minimal probability.     

IEEE 1394火线技术与USB串行接口的比较

在市场发展的需求下，产生了IEEE 1394和USB两种通用外设接口标准，这两种接口既有相同之处，又各有所长。为了能更好地掌握其技术应用，这里论述了这两种串行接口的产生。发展及它们各自的特点，讨论了两者的异同之处，并在文章的最后指出了将来的发展方向，对不同的接口应用有一定的参考价值。     

HB协议的形式规约与验证

形式化方法是确保安全协议设计正确性的重要工具,利用形式化方法已经发现了许多安全协议的设计错误.首次利用形式规约语言Z对RFID安全协议HB进行形式规约, 并对HB协议应该满足的安全性质进行形式化描述,使用Z模式推理从协议及其运行环境两个方面验证了协议的关键安全属性,发现了HB协议在设计方面的缺陷,提出了HB协议的一种改进方法.     

一种IEEE 1394b主机光纤接口卡的设计与实现

针对工控领域中对现场总线传输距离、抗电磁干扰性、总线带宽方面的要求,设计了一种具有故障诊断功能的IEEE 1394b-PCI先纤接口卡.利用此接口卡搭建光总线系统进行实验测试.由实验得到的工控机端光总线视频传输图及实验数据,可以看出该接口卡能够满足实际的应用需求.同时,搭建的光总线系统能够实现故障定位,方便现场维护.     

基于AS5643协议的Mil-1394仿真卡设计与实现

仿真卡是现代地面仿真系统的重要组成部分,Mil-1394仿真卡则在机载军用1394总线网络地面仿真系统中发挥着非常重要的作用。结合军用航空领域广泛应用的SAEAS5643协议,文中系统性地介绍了一种Mil-1394总线仿真卡的解决方案,叙述了其硬件和逻辑构架,详细阐述了仿真卡的软件设计,并进行了大量的仿真实验和数据分析。实验结果充分表明该仿真卡达到了较高的传输速率,功能完备,性能良好,全面满足地面仿真系统的应用需求。     

A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol

The IEEE 1394 tree identify protocol illustrates the adequacy of the event-driven approach used together with the B Method. This approach provides a complete framework for developing mathematical models of distributed algorithms. A specific development is made of a series of more and more refined models. Each model is made of a number of static properties (the invariant) and dynamic parts (the guarded events). The internal consistency of each model as well as its correctness with regard to its previous abstraction are proved with the proof engine of Atelier B, which is the tool associated with B. In the case of IEEE 1394 tree identify protocol, the initial model is very primitive: it provides the basic properties of the graph (symmetry, acyclicity, connectivity), and its dynamic parts essentially contain a single event which elects the leader in one shot. Further refinements introduce more events, showing how each node of the graph non-deterministically participates in the leader election. At some stage in the development, message passing is introduced. This raises a specific potential contention problem, whose solution is given. The last stage of the refinement completely localises the events by making them take decisions based on local data only. Received July 2001/Accepted in revised form October 2003 Correspondence and offprint requests to: Dominique Méry, Université Henri Poincaré Nancy 1, LORIA, BP239, 54506 Vandœuvre-lès-Nancy Cedex, France. Email: mery@loria.fr     

基于Verilog HDL的IEEE1394协议中CRC校验的实现

CRC是IEEE1394协议中重要的错误检测和恢复机制。介绍循环冗余校验的基本原理,根据IEEE1394协议中CRC码的产生原理．分析CRC校验的具体计算过程,讨论IEEE1394协议中CRC的FPGA实现．借助EDA工具和Verilog HDL语言实现了对这．种算法的仿真和验证。     

1394总线在实时图像系统中的应用

随着红外成像技术的不断发展,红外图像的数据量越来越大,成像的速度也越来越快,这就要求红外成像系统具有实时采集、实时处理、实时传送大批量数据的能力;但是现有的大部分数据传输接口速率较低,难以满足现实中对速度越来越高的要求;将1394高速申行接口引人到红外成像系统中,完成了1394接口电路硬件及软件的设计,并在微控制器(MCU)和FPGA的控制下实现了红外图像的高速传输、实时显示,大大提高图像数据的采集速度和系统的整体性能;测试结果表明,通过1394总线每秒可以传输42帧大小为320 * 240的红外图像,并实现了图像的实时清晰显示,满足了红外成像系统实时采集实时显示红外图像的要求.     

IEEE1394技术及其发展综述

简要回顾了IEEE1394的技术背景及其基本特性,介绍了IEEE1394串行总线标准和连接方式,此外还讨论了IEEE1394的应用范围和发展前景。     

基于IEEE1394总线的图像采集处理系统实现

针对卫星激光通信的瞄准捕获跟踪(PAT)系统的图像处理子系统对光信号的检测要求处理速度快,抗干扰能力和实时性强等特点,设计了基于IEEE1394总线的图像采集处理系统来接收CCD传出的图像数据。采用CCD摄像机作为整个系统的光信号探测器,并利用基于IEEE1394总线的图像采集处理系统来接收CCD传出的图像数据。采用了数字信号处理器DSP作为图像处理系统的主控单元,并采用了两片1394芯片分别实现链路层和物理层。对于系统的软件设计,根据角偏差算法的特点,设计处理数据方式为:每采集一个等时数据包就对该数据包进行处理并将结果累加,到下一幅图像传输开始时完成对上一幅图像的处理。经调试,该系统成功应用于卫星激光通信试验系统的激光束位置偏差信号的检测,它具有硬件实现简单,处理速度快,软件升级性好等特点。     

False Loop Detection in the IEEE 1394 Tree Identify Phase

The physical layer of the IEEE 1394 (FireWire, i-Link) architecture contains a protocol for spanning a tree in the network topology, which fails if the topology contains a loop. We show that the timing requirements for both the 1394-1995 and 1394a-2000 standards are too lenient: these allow for scenarios in which there is no loop in the topology, but the tree-spanning protocol does detect one. The scenarios are found by the model checker UPPAAL. Received August 2001/Accepted in revised form August 2001 Correspondence and offprint requests to: J. M. T. Romijn, Computing Science Department, Eindhoven University of Technology, PO Box 513, 5600 MB Eindhoven, The Netherlands. Email: J.M.T.Romijn@tue.nl     

使用组合协议逻辑PCL验证Amended Needham-Schroeder协议

安全协议的形式化分析和验证一直是信息安全领域的一个重要问题。本文介绍了组合式验证方法以及面向安全协议验证的组合式验证工具PCL,并采用PCL对Amended Needham-Schroeder协议进行了验证,证明该协议满足保密性。在验证中将完整的协议划分为三个子协议,对子协议分别做性质描述和验证,最后将三个子协议组合成完整的协议,通过三个子协议之间前置断言和后置断言的一致性,证明了组合之后的协议满足保密性。     

星载设备IEEE1394总线PC端通信程序的设计与实现

结合IEEE1394总线规范,介绍了在Windows XP环境下利用微软驱动程序开发套件(DDK)开发IEEE1394设备驱动程序的设计原理,讨论了如何利用DDK提供的设备诊断驱动程序实现1394异步通信与等时通信程序的设计,给出了PC端通信程序的设计方法,最后结合工程实例表明了程序的可行性.     

基于1394总线通信的I/O模块在数控系统中的应用

设计了一种基于IEEE 1394总线通信,应用于高档数控系统中的I/O控制模块.该模块采用IEEE 1394通信方式,实现上位机与机床之间的高速数据传榆;采用光耦芯片对模块内部与外界进行隔离,并实现该I/O模块与机床之间的电平匹配,模数转换等功能.给出了软件和硬件设计,并进行了I/O模块功能测试和分析,验证了该模块满足高档数控系统要求数据传输的准确性和实时性.     

IEEE1394协议在外设端接口中的应用

为了提高大幅面彩色喷墨绘图机的接口速度,对IEEEl394协议进行了研究。文章首先介绍了IEEEl394协议的传输类型以及物理层、链路层、事务层和总线管理层的功能。然后结合IEEEl394外设端接口板的开发,给出了IEEEl394通讯接口的一种设计方案及驱动的编程方法。最后对IEEEl394协议的应用做了展望。     

多agent逻辑程序及其在协议验证中的应用

提出一种多agent逻辑程序,每个agent具有一个相信算子,讨论了其不动点语义和操作语义,证明了两种语义之间的等价性.提出了一种基于多agent逻辑程序的协议验证方法,以一种多方非否认安全协议为例,对该协议进行了形式化描述,验证了其具有不可否认性.     

Design and implementation of a vehicle interface protocol using an IEEE 1394 network

A wide variety of in-vehicle devices such as camera sensors, navigation systems, telematics and communication equipments have been incorporated into a vehicle to realize Intelligent Transport Systems (ITS) applications. Because an efficient standardized network is required, ITS Data Bus (IDB) has been discussed to carry high-speed multimedia data for audio, video and other real-time ITS applications. For connecting devices in a standardized manner, the IDB network has architecture with a gateway called vehicle interface which is located between automaker’s proprietary network and the standardized IDB network. IEEE 1394 (also known as iLink or FireWire), which can transport multimedia data for consumer electronics, is a good candidate for IDB network. In this paper, we analyze the issues for existing AV/C protocol (application layer protocol over IEEE 1394) to comprise the IDB network. In addition, we designed and implemented the vehicle interface protocol as a higher layer of IEEE 1394 to address the AV/C protocol issues for realizing the whole IDB network architecture.