Sensors and actuators in TCOZ

Timed Communicating Object Z (TCOZ) combines Object-Z's strengths in modeling complex data and algorithms with Timed CSP's strengths in modeling real-time concurrency. TCOZ inherits CSP's channel-based communication mechanism, in which messages represent discrete synchronisations between processes. The purpose of most control systems is to observe and control analog components. In such cases, the interface between the control system and the controlled systems cannot be satisfactorily described using the channel mechanism. In order to address this problem, TCOZ is extended with continuous-function interface mechanisms inspired by process control theory, the sensor and the actuator. The utility of these new mechanisms is demonstrated through their application to the design of an automobile cruise control system.