A Timed Verification of the IEEE 1394 Leader Election Protocol

The IEEE 1394 architecture standard defines a high performance serial multimedia bus that allows several components in a network to communicate with each other at high speed. In the physical layer of the architecture, a leader election protocol is used to find a spanning tree with a unique root in the network topology. If there is a cycle in the network, the protocol treats this as an error situation. This paper presents a formal model of the leader election protocol in the language IOA and a correctness proof. Hereby, it is shown that under certain timing restrictions the protocol behaves correctly. The timing parameters in the IEEE 1394 standard documentation obey the restrictions found in this proof.     

Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k

This paper reports on the mechanical verification of the IEEE 1394 root contention protocol. This is an industrial leader election protocol, in which timing parameters play an essential role. A manual verification of this protocol using I/O automata has been published in [24]. We improve the communication model presented in that paper. Using the Uppaal2k tool, we investigate the timing constraints on the parameters which are necessary and sufficient for correct protocol operation: by analyzing large numbers of protocol instances with different parameter values, we derive the required timing constraints. We explore the use of model checking in combination with stepwise abstraction. That is, we show that the implementation automaton correctly implements the specification via several intermediate automata, using Uppaal to prove the trace inclusion in each step. Published online: 18 July 2001     

Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention Protocol

The interplay of real time and probability is crucial to the correctness of the IEEE 1394 FireWire root contention protocol. We present a formal verification of the protocol using probabilistic model checking. Rather than analyse the functional aspects of the protocol, by asking such questions as ‘Will a leader be elected?’, we focus on the protocol's performance, by asking the question ‘How certain are we that a leader will be elected sufficiently quickly?’ Probabilistic timed automata are used to formally model and verify the protocol against properties which require that a leader is elected before a deadline with a certain probability. We use techniques such as abstraction, reachability analysis and integer-time semantics to aid the model-checking process, and the efficacy of these techniques is compared. Received July 2001/Accepted in revised form November 2002 Correspondence and offprint requests to: Marta Kwiatkowska, School of Computer Science, University of Birmingham, Birmingham B15 2TT, UK. Email: M.Z.Kwiatkowska@cs.bham.ac.uk     

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     

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 forwards 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 how this minimal probability is influenced by using a biased coin and considering different wire lengths.     

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     

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.     

一种IEEE1394物理层IP的FPGA原型验证方法

符合IEEE1394协议的物理层IP主要完成总线连接检测、连接管理、仲裁、数据收发等功能,是一款集成高速Ser-des的数模混合SoC。由于在Serdes的测试芯片设计完成前无法对1394物理层IP进行全面验证,因此文中在介绍1394 PHY物理层IP各部分功能的基础上,提出了一种以Xilinx的GTP代替1394物理层Serdes,构建FPGA原型验证平台,采用专用硬件逻辑和软件结合的方式,对1394物理层IP进行充分验证的方法。使用该平台可在Serdes设计未完成前对数字逻辑进行验证,大大缩短物理层IP的开发周期;通过软件控制下的测试项生成、测试过程监控、测试结果判断,可显著提高验证效率。     

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     

Using SPIN to Analyse the Tree Identification Phase of the IEEE 1394 High-Performance Serial Bus (FireWire) Protocol

We describe how the tree identification phase of the IEEE 1394 high-performance serial bus (FireWire) protocol is modelled in Promela and verified using SPIN. The verification of arbitrary system configurations is discussed. Received July 2001/Accepted in revised form November 2002 Correspondence and offprint requests to: Alice Miller, Department of Computing Science, University of Glasgow, 17 Lilybank Gardens, Glasgow G12 8QQ, UK. Email: alice@dcs.gla.ac.uk     

A Self-Stabilizing Leader Election Algorithm for Tree Graphs

We propose a self-stabilizing algorithm (protocol) for leader election in a tree graph. We show the correctness of the proposed algorithm by using a new technique involving induction.     

Fun with FireWire: A Comparative Study of Formal Verification Methods Applied to the IEEE 1394 Root Contention Protocol

Formal Aspects of Computing - The IEEE 1394 Root Contention Protocol is an industrial leader election algorithm for two processes in which probability, real time and parameters play an important...     

基于串空间的安全协议自动化验证算法

以串空间模型为理论基础,提出安全协议自动化验证算法IVAP。对于有漏洞的协议,针对不安全属性逆向搜索主体串树,自动生成改进协议并对其进行验证,直至生成一个安全的改进协议。实验结果证明了该自动化验证算法的有效性,与AAAP算法相比,其协议验证效率更高。     

多任务并行IEEE1394协议栈设计

为满足嵌入式系统对高可靠性和实时性的要求,利用IEEE1394总线标准的软硬件特性,设计多任务并行IEEE1394协议栈,通过设置不同任务优先级获得不同服务质量的数据传输,从而使IEEE1394子系统任务和命令的执行更具实时性。在VxWorks平台上实现的基于该协议栈的数字视频解码与SBP2移动存储验证了该设计的可行性。     

光总线系统网络拓扑结构的可靠性分析

光总线精确制导控制与测试系统具有技术难度大、系统性强、所处环境恶劣,电磁兼容性要求高的特点.要有效地保障系统预定任务的顺利执行和完成,提高战斗出勤率,因此,IEEE-1394b 光总线系统必须是高可靠的、高稳定的.分析研究IEEE-1394b光总线拓扑的可靠性实验研究,是解决IEEE-1394b 光总线系统可靠性问题的重要内容之一.提出了基于IEEE-1394b 协议的光总线网络拓扑结构的可靠性研究方案,建立了环状拓扑可靠性分析模型,并给出了示例分析.实验结果表明,这种环状拓扑结构具有高的可靠性.     

一种基于攻击序列求解的安全协议验证新算法

基于完美加密机制前提及D-Y攻击者模型,指出注入攻击是协议攻击者实现攻击目标的必要手段.分析了注入攻击及其形成的攻击序列的性质,并基于此提出了搜索攻击序列的算法,基于该算法实现了对安全协议的验证.提出和证明了该方法对于规则安全协议的搜索是可终止的,并通过实验实现了NS公钥协议的验证.实验结果表明,与OFMC等同类安全协议验证工具相比,该算法不仅能实现安全协议验证自动化,而且由于规则安全协议验证的可终止性,使得本算法更具实用性.     

Model checking mobile ad hoc networks

Modeling arbitrary connectivity changes within mobile ad hoc networks (MANETs) makes application of automated formal verification challenging. We use constrained labeled transition systems as a semantic model to represent mobility. To model check MANET protocols with respect to the underlying topology and connectivity changes, we introduce a branching-time temporal logic. The path quantifiers are parameterized by multi-hop constraints over topologies, to discriminate the paths over which the temporal behavior should be investigated; the paths that violate the multi-hop constraints are not considered. A model checking algorithm is presented to verify MANETs that allow arbitrary mobility, under the assumption of reliable communication. It is applied to analyze a leader election protocol.     

Trie+结构函数式建模、机械化验证及其应用

Trie结构是一种使用搜索关键字来组织信息的搜索树,可用于高效地存储和搜索字符串集合.T.Nipkow给出了实现Trie的Isabelle建模与验证,然而其Trie在存储和操作时存在大量的冗余,导致空间利用率不高,且仅考虑英文单模式下查找.为此,本文基于索引即键值的思想提出的Trie+结构,相较于传统的索引与键值分开存储的结构能减少50%的存储空间,大大提高了空间利用率.并且,对Trie+结构的查找、插入、删除等操作给出了函数式建模及其严格的机械化验证,保证操作的正确性和可靠性.进一步,首次提出一种匹配算法的通用验证规约,旨在解决一系列的匹配算法正确性验证问题.最后,基于Trie+结构与匹配算法通用验证规约,建模和验证了函数式中英文混合多模式匹配算法,发现并解决了现有研究中的基于完全哈希Trie的多模式匹配算法的模式串前缀终止的Bug.所提的Trie+结构以及验证规约在提高Trie结构空间利用率和验证匹配算法中,有一定的理论和应用价值.