A Formal design technique for real-time embedded systems development using duration calculus.

In this paper we present a syntactical approach for the design of real-time embedded systems. The require- ment of the system is specified as Duration Calculus formula over continuous state variables. We model discretization at the state level and approximate continuous state variables by discrete ones. The discrete design is formulated as Du- ration Calculus formula over discrete state variables. The correctness of the design can be established using composi- tional proof rules. A real-time program is then derived from the discrete design using an extension of the assumption- commitment paradigm to real-time. We illustrate our ap- proach using a simple water tank control system