The temporal Boolean derivative applied to verification of extended finite state machines

Extended finite state machines are an important feature of modern computers. Their verification, unlike sequential system testing, is very complex and has received little attention in literature. This paper suggests a model based on a symbolic representation to describe the temporal behavior of sequential machines. Two examples of different architectures illustrate the application of the methodology.