Benchmark Hybrid Systems

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