The formal design of distributed controllers with d SL and Spin
Bram De Wachter, Alexandre Genon, Thierry Massart, Cédric Meuter · Formal Aspects of Computing · 2005
Abstract We study the formal verification of programs written in d SL, an extension of the standard ST language used to program industrial controllers. It proposes a trade off between industrial and formal verification worlds. The main advantage of d SL is to provide a transparent code distribution through low level communication mechanisms. The behavior of the synthesized distributed system can therefore be formally modeled, easily monitored and formally verified. The verification of a d SL program, realized with the Spin tool, is eased by the definition of a lattice of models linked with a simulation relation preserving next-free LTL formulae. We show that, although d SL is an industrial programming language, it gives the possibility to verify systems designed with it. We illustrate the benefit of our approach with a simple control system of two canal locks.