In this paper, we present an application of syntactical approach given in a formal design technique for real-time embedded systems. The technique is the model of discretization at the state level and the approximation of continuous state variables by discrete ones. The lift system presented in this paper shall be monitored and controlled by a computing system that shall respect the components, handle the events, and satisfy the usual procedures and invariants. The Duration Calculus with Iteration is used in the paper to specify requirements of the system.

Tải file Designing a lift control system tại đây