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 |
|---|---|---|---|---|
| Thermostat | A basic thermostat. | Temperature x remains within t1 and t4 bounds. Average time in On state. | Invariance | |
| 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 | Scale-independent hysteresis switching logic for supervisory controller. | Stability | Average dwell time, implementation relation | Liberzon |
| Alice | Controller-Vehicle subsystems of an autonomous ground vehicle. | Safety and Progress | ||
| Pattern formation | Distributed coordination of mobile agents. | Invariance and Progress | Convergence to target pattern | Chandy, Mitra, Pilotto |