Asynchronous Mid-Value Select in Hybrid SAL

The following SAL model is an abstraction of a module that implements a fault-tolerant mid-value select on asynchronously produced inputs. This is part of a larger system that has both discrete and continuous dynamics, Our goal is to model the full system using Hybrid SAL and we have adapted the timed relational abstraction techique supported by Hybrid SAL to abstract asynchronous sampling of continous signals. This approach will be fully automated in future releases of Hybrid SAL.

The following model (05/14/2012) shows the resulting abstraction, for the aysnchronous mid-value select module and includes proofs of various properties.