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     

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     

Comparison of SPIN and VIS for protocol verification

In this paper, we compare and contrast SPIN and VIS, two widely used formal verification tools. In particular, we devote special attention to the efficiency of these tools for the verification of communications protocols that can be implemented either in software or hardware. As a basis of our comparison, we formally describe and verify the Asynchronous Transfer Mode Ring (ATMR) medium access protocol using SPIN and its hardware model using VIS. We believe that this study is of particular interest as more and more protocols, like ATM protocols, are implemented in hardware to match high-speed requirements. Published online: 1 March 2002     

小额交易中SET协议的优化及SPIN验证的研究

作为电子商务的重要组成部分,基于Internet的电子交易受到了广泛的关注。SET交易过程十分复杂,在完成一次SET协议交易过程中,需验证电子证书9次,验证数字签名6次,传递证书7次,进行签名5次,4次对称加密和非对称加密。本文选取SET协议的核心部分：购买请求、支付认证和获得付款3个子协议过程作为研究分析对象,针对不同数额的交易进行分级,针对小额的交易过程进行协议的优化,对SET进行SPIN模型检测,并根据分析模拟与验证的结果对SET进行改进。     

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     

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...     

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     

Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN

The General Inter-Orb Protocol (GIOP) is a key component of the Common Object Request Broker Architecture (CORBA) specification. We present the formal modeling and validation of the GIOP protocol using the Promela language, Linear Time Temporal Logic (LTL) and the Spin model checker. We validate the Promela model using ten high-level requirements which we elicit from the informal CORBA specification. These requirements are then formalized in LTL and the Spin model checker is used to determine their validity. During the validation process we discovered a few problems in GIOP: a potential transport-layer interface deadlock and problems with the server migration protocol. We also describe how property specification patterns helped us in formalizing the high-level requirements that we have elicited.     

Automatic Verification of a Lip-Synchronisation Protocol Using Uppaal

We present the formal specification and verification of a lip-synchronisation protocol using the real-time model checker Uppaal. A number of specifications of this protocol can be found in the literature, but this is the first automatic verification. We take a published specification of the protocol, code it up in the Uppaal timed automata notation and then verify whether the protocol satisfies the key properties of jitter and skew. The verification reveals some aws in the protocol. In particular, it shows that for certain sound and video streams the protocol can time-lock before reaching a prescribed error state. We also discuss our experience with Uppaal, with particular reference to modelling timeouts and to deadlock analysis. Received March 1998 / Accepted in revised form October 1998     

Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checker

Statechart Diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modelling Language (UML). In this paper we present a translation from a subset of UML Statechart Diagrams - covering essential aspects of both concurrent behaviour, like sequentialisation, parallelism, non-determinism and priority, and state refinement - into PROMELA, the specification language of the SPIN model checker. SPIN is one of the most advanced analysis and verification tools available nowadays. Our translation allows for the automatic verification of UML Statechart Diagrams. The translation is simple, proven correct, and promising in terms of state space representation efficiency. Received September 1999 / Accepted in revised form February 2000     

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     

Validating the PSL/Sugar Semantics Using Automated Reasoning

The Accellera organisation selected Sugar, IBMs formal specification language, as the basis for a standard to drive assertion-based verification in the electronics industry. Sugar combines regular expressions, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL) into a property language intended for both static verification (e.g. model checking) and dynamic verification (e.g. simulation). In 2003 Accellera decided to rename the evolving standard to Accellera Property Specification Language (or PSL for short). We motivate and describe a deep semantic embedding of PSL in the version of higher-order logic supported by the HOL 4 theorem-proving system. The main goal of this paper is to demonstrate that mechanised theorem proving can be a useful aid to the validation of the semantics of an industrial design language.     

Using symbolic CTL model checking to verify the railway stations of Hoorn-Kersenboogerd and Heerhugowaard

We examine the application of symbolic CTL model checking to railway interlocking software. We show that the railway interlocking systems examined exhibit the characteristics of robustness and locality, and that these characteristics allow optimizations to the model checking algorithms not possible in the general case. In order to gain a better understanding of robustness and locality, we examine in detail a small railway interlocking. Published online: 9 October 2001     

Preface by the section editor

The papers in this special section present a sampling of new symbolic approaches for determining whether or not a system satisfies its specification. Abstracts of these articles appeared originally in the Proceedings of the 1999 Symposium on Tools and Algorithms for the Construction and Analysis of Systems (TACAS ’99). Published online: 18 July 2001     

Verification of the Multistream Protocol (MSP) using COSPAN

This article presents the verification of several key properties of the MultiStream Protocol (MSP), a new feature-rich transport protocol. The verification was performed using the Coordination Specification Analyzer (COSPAN). The verification of this protocol presented many challenges due to the complexity of the protocol and its implementation architecture