Safety property verification of Esterel programs and applications to telecommunications software

Abstract

We present a technique for automatically verifying linear-time temporal logic safety properties of programs written in Esterel, a formally-defined language for programming reactive systems. In our approach, linear-time temporal logic safety properties are first translated into Esterel programs that model these properties. Using the Esterel compiler, the translations are compiled in parallel with the Esterel program to be verified. A trivial reachability analysis of the output of the compiler then indicates whether or not the safety property is satisfied by the program. We describe two real-world software problems — Esterel versions of two features of the AT&T 5ESS® switching system — and one well-known benchmark problem — the generalized railroad crossing problem — that we have verified using our technique and associated tool set.