This monograph presents a framework for modelling, specifying and verifying systems composed of real-time discrete event processes. A discrete event system consists of the plant (the object to be controlled) and a controller. For example, the plant might consist of machines, robots and conveyors on the factory floor. The objective of a computer controller might be to command the robots to move parts from machines to conveyors in some required fashion, without colliding into other objects. Extended state machines (ESMs) are used to model the processes and devices of the plant, as well as the software tasks of controllers implemented as real-time software. Real-time temporal logic (RTTL) is used to specify required plant behaviour, and to verify that the controller achieves the specification. The ESM/RTTL framework has a proof system, semi-automated help and heuristics for constructing proofs, and decision procedures for finite state systems.

This book is addressed to: • software engineers and researchers especially those interested in safety- critical, real-time systems, and • control engineers who are interested in extending control theoretic concepts to discrete event systems.

An initial version of some of this work appeared in my thesis [64]. Although by its nature the framework developed in this book must be regarded as somewhat exploratory and tentative, the intent of this publication is to make the work available to a larger audience in a timely fashion.