Verifying Relay Circuits using State Machines

Abstract

In this paper we present, illustrate and discuss a number of techniques that can be used in the modelling and verification of electro-mechanical relay circuits. These techniques are based on state machine descriptions of circuits and their functions, and on applying validation tools for properties of such descriptions. In particular we have applied tools that are based on the PROMELA language.