Verifying Relay Circuits using State Machines
P.H.J. van Eijk · 1997
In this paper we present 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 apply validation tools for such descriptions. Key words & Phrases: formal specification, formal verification, safety critical system, relay, state machines, PROMELA. 1 Introduction For any artefact that is designed, the question sooner or later comes up: "If we build it this way, will it do what we want it to do?" This is the correctness question, and the answer to it can be a matter of life and death. In this paper we will see how current technology for verifying correctness can be applied to relatively old hardware technology. It will become apparent that correctness of relay circuits is a topic with many sides, and many levels. On each of these levels there are a number of techniques that can be applied. This paper is subdivided in the followi...