SAL Examples


Timed-Triggered Ethernet in SAL

The following SAL files model some aspects of the fault-tolerant clock-synchronization protocol used in Timed-Triggered Ethernet (TTE). They mostly focus on the impact of a small change to the TTE compression function.

Other SAL models of TTE are described in the SAL Wiki's TTEthernet Section.

Hybrid SAL Relational Abstractor

The following tar file contains tools for the analysis of hybrid systems using abstraction. The distribution includes source code, documentation, and several examples. Related background material and publications are available on Ashish Tiwari's web page on relational abstraction.


Timed model of the TTA Startup Protocol in SAL

The following SAL files illustrate the application of calendar automata to the modeling of real-time systems. Both are inspired from the TTA fault-tolerant startup protocol. The verification builds an abstraction of the protocol that is proved correct using the SAL infinite-state, bounded model checker. A correctness property is then derived from the abstraction.

Simplified version: no faults

Version with one faulty node (no faulty hub yet)

Minor variant, with a slightly different hub model