From Continuous Specification to Discrete Design

摘要

The paper presents a syntactical approach to designing 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 formalise the relationship between them. The requirements of a real-time system are specified as a formula over continuous state variables. Then we derive a discrete design of a digital controller as formula over discrete stat variables that makes the system to satisfy the continuous specification under some assumptions about the behaviour of the environment and the relation-ship between continuous state variables and discrete state variables. We provide rules useful for refining and verifying the correctness of a design syntactically.