Here is a collection of hybrid systems specified in the TIOA language. Other examples and more details on how different analysis tools perform on these examples will be posted soon. Send me email to add your favorite examples.
| Name | Description | Goal | Type | Source |
|---|---|---|---|---|
| TimedChannel | A delay prone FIFO channel. Used in other specifications. | Timely delivery of messages | Invariant | |
| ClockSync | A follow-the-leader type clock synchronization algorithm for a set of processes with drifting clocks. | Validity and agreement of logical clocks | Invariant | |
| FailureDetector | A simple timeout-based failure detector over delay-prone communication channel. | Soundness and timeliness of failure detector | Implementation relation | |
| OneShotController | A one-shot controller for a vehicle deceleration manuver. | Safety (velocity range) and liveness | Invariants and implementation relation | Weinberg, Lynch, et al. |
| Quanser (coming soon!) | Supervisory pitch-controller for a model helicopter rotor system manufactured by Quanser. | Safety | Invariants and implementation relation | Mitra, Wang, Lynch, Feron |
| HysSwitch (coming soon!) | Scale-independent hysteresis switching logic for supervisory controller. | Stability | Average dwell time, implementation relation | Liberzon |