Technical Reports

The ICICS/CS Reading Room

UBC CS TR-93-04 Summary

Design and Analysis of Embedded Real-Time Systems: An Elevator Case Study, February 1993 Yang Zhang and Alan K. Mackworth, 44 pages

Constraint Nets have been developed as an algebraic on-line computational model of robotic systems. Timed forall-automata have been studied as a logical specification language of real-time behaviors. A general verification method has been proposed for checking whether a constraint net model satisfies a timed forall-automaton specification. In this paper, we illustrate constraint net modeling and timed forall-automata analysis using an elevator example. We start with a description of the functions and user interfaces of a simple elevator system, and then model the complete system in Constraint Nets. The analysis of a well-designed elevator system should guarantee that any request will be served within some bounded time. We specify such requirements in timed forall-automata, and show that the constraint net model of the elevator system satisfies the timed forall-automaton specification.

If you have any questions or comments regarding this page please send mail to