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