VVFCS Project

This page presents PVS and SAL models of fault-tolerant distributed systems developed by SRI as part of a NASA-funded project on the modeling and analysis of fault-tolerant distributed systems. This project is part of NASA's effort on Verification and Validation of Flight-Critical Software.


Models of the TTEthernet Synchronization Protocol

Timed-Triggered Ethernet (or TTEthernet)is a communication infrastructure that enables the use of Ethernet in real-time, distributed systems. TTEthernet is compatible with traditional IEEE 802.3 switched Ethernet standards, and is designed to support dataflows of mixed criticality on a single network. For traffic of the highest criticality, TTEthernet provides a timed-triggered communication service that relies on a fault-tolerant clock-synchronization protocol.

We have developed formal models of parts of the TTEthernet protocols and analyzed safety-critical properties using both SAL and PVS. Related work by Wilfried Steiner is described in the SAL Wiki.

SAL Models (02/11/2012)

The following SAL specifications focus on TTEthernet's compression function. They show that better synchronization can be achieved by a simple change to the original TTEthernet definition.


PVS Models (02/11/2012)

The following PVS file contains a general specification of TTEthernet's compression function and proofs of several important properties. The specification and proofs were developed using PVS 5.0.

Draper Clock-Synchronization Protocol in SAL

In 1973, Daly, Hpokins, and McKenna (from Draper Lab.) presented a fault-tolerant digital clocking system at the FTCS conference. This is probably one of the first published system designs that is intended to tolerate arbitrary, asymmetric faults (i.e., Byzantine faults).

The following SAL models (05/14/2012) are two variant formalizations of this Draper Clock-Synchronization Protocol developed by Ashish Tiwari.

We also used QBF solvers to synthesize deterministic Byzantine consensus procedures. The following SAL models (08/19/2013) were used to perform synthesis. Note that the models have uninitialized parameters - and hence SAL will be unable to prove anything interesting about them. The models were used as automatically construct an input for a QBF solver. Brief summary of the synthesis results: In general, most synthesis results were negative; i.e., there exist no deterministic Byzantine fault-tolerant consensus algorithms. For case when faulty clock is disallowed ONE specific behavior, we can synthesize a deterministic consensus algorithm. When the faulty clock can send values in the set {Null,1} or in the set {Null,0}, but not values in the set {0,1}, then the result is the same: no deterministic algorithm exists. If we force the faulty clock to also 'behave' and follow the protocol that the good clocks are following, and then send values from {Null,1} if its value is 1 and values from the set {Null,0} if its value is 0, then the result, surprisingly, is STILL THE SAME. If bad clock is forced to remain bad in the same way for 2 time steps, then we get a positive result: in fact, two different solutions were synthesized.

Asynchronous Mid-Value Select in Hybrid SAL

The following SAL model is an abstraction of a module that implements a fault-tolerant mid-value select on asynchronously produced inputs. This is part of a larger system that has both discrete and continuous dynamics, Our goal is to model the full system using Hybrid SAL and we have adapted the timed relational abstraction techique supported by Hybrid SAL to abstract asynchronous sampling of continous signals. This approach will be fully automated in future releases of Hybrid SAL.

The following model (05/14/2012) shows the resulting abstraction, for the aysnchronous mid-value select module and includes proofs of various properties.


Tempo2HSal - Converter from Tempo to HybridSal

A converter for translating models written in Tempo to models in HybridSal.