Ecole Polytechnique Fédérale de Lausanne
english only

HyTech Demo Menu

Please choose your input example. You may use an example in our test set or design your own example.

Railroad gate controller
The gate controller of a railroad crossing has a delay of a seconds; that is, the gate starts closing a seconds after a train signals its approach. HyTech computes the safe values of a such that the gate is fully closed whenever the train is within 10 meters of the gate. (PostScript illustration.)

Timing-based mutual-exclusion protocol
Fischer's shared-variables protocol relies on timing to ensure mutual exclusion between two processes. HyTech computes the safe values for the duration a of shared-memory accesses and the duration b of explicit delays, assuming that all durations are measured by drifting local clocks. (PostScript illustration.)
Design your own example

- Back to the HyTech home page
- For questions and comments send mail to hytech-AT-epfl.ch
Last updated in April, 2006