| Publisher | Universität Ulm | ||
|---|---|---|---|
| Format | 133.0KB PostScript, requires PS viewer | Date added | 17 Jan 1999 |
| Topics | Industry Standard Protocols, Computer Testing Equipment | ||
| Downloads | 29 | ||
Distributed dependable real-time systems crucially depend on fault-tolerant clock synchronization. This paper reports on the formal analysis of the clock synchronization service provided as an integral feature by the Time-Triggered Protocol (TTP), a communication protocol particularly suitable for safety-critical control applications, such as in automotive "by-wire" systems. We describe the formal model extracted from the TTP specification and its formal verification, using the PVS system. Verification of the central clock synchronization properties is achieved by linking the TTP model of the synchronization algorithm to a generic derivation of the properties from abstract assumptions, essentially establishing the TTP algorithm as a concrete instance of the generic one by verifying that it satisfies the abstract assumptions. We also show how the TTP algorithm provides the clock synchronization that is required by a previously proposed general framework for verifying time-triggered algorithms.
Did you find this white paper useful?
16 out of 39 users found this white paper useful
Related white papers
Technology Marketing Case Study: Coleman County Co-Op Converts Triple Play
The client was Coleman County Telephone Cooperative, Inc. (CCTC). Through extensive industry research and a careful forward looking revenue forecast it became evident that the careful deployment of an IP-based...
Case Study: Design and Development of Silhouette 1.0
Natural Convergence Inc. (NCI) develops and markets hosted VoIP software solutions. NCI is developing a voice over IP framework that enables service providers to deliver IP voice services to small...
Tone Based MAC Protocol for Use With Adaptive Array Antennas
This paper presents a novel Tone-based 802.11b protocol for use in wireless networks where nodes are equipped with adaptive array antennas. The protocol relies on the ability of the antenna...
GPRS White Paper
The General Packet Radio System (GPRS) is a new service that provides actual packet radio access for mobile Global System for Mobile Communications (GSM) and time-division multiple access (TDMA) users....
SIP: Protocol Overview
The Session Initiation Protocol (SIP) is a signaling protocol for initiating, managing and terminating voice and video sessions across packet networks. SIP sessions involve one or more participants and can...
Layer 3 Malformed Packet Testing in MCI's Public IP Network
Malformed packets associated with routing protocols can cause undesirable consequences if not detected and contained properly as close to the originator as possible. This issue magnifies in scope and complexity...
Delivering Unique Services that Meet Customer Needs
The telecommunications industry is rapidly re-inventing itself to meet its changing and expanding role in the business world. With the advent of cellular, WiFi, WiMax and increasingly powerful and...
