A Solution to the Generalized Railroad Crossing Problem in ESTEREL
Carlos Puchol · 1995
We present a solution to the Generalized Railroad Crossing benchmark problem based on the ESTEREL programming language. The solution is shown to satisfy the formal statements of the properties that the system requirements specify by using a verification method for safety properties of ESTEREL programs recently developed. The solution and verification presented have been developed within the synchronous system model, i.e. discrete time, global broadcast of events and instantaneous reactions. Keywords: ESTEREL, reactive systems, synchronous systems, system verification, systems specification, formal methods. 1 The Generalized Railroad Crossing Problem The Generalized Railroad Crossing (GRC) problem is a benchmark problem that has been recently proposed [4] to compare formal methods that exist for specifying, designing and analyzing real-time systems and to better understand their utility in the development of practical systems. Informally, it consists of a gate controlling a rai...