From continuous specification to discrete design.
François Siewe, Dang Van Hung · 2000
In this report we present a syntactical approach to the design of real-time distributed systems that can handle both continuous time and discrete time models in a uniform logical framework. We approximate continuous state variables by discrete ones and formalize the relationship between them. Given a specification of the requirements of a real-time system as a formula over continuous state variables, we derive a discrete design of a digital controller as formula over discrete state variables that makes the system to satisfy the continuous specification under some assumptions about the behavior of the environment and the relationship between continuous state variables and discrete state variables. We provide rules useful for refining and verifying the correctness of an implementation syntactically. Francois Siewe is a Fellow of UNU/IIST (May to December 1999), on leave from the Department of Mathematics and Computer Science, University of Dschang, Cameroon, where he is a lecturer. He ...