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.

Abstract In a basic agent calculus, equality often links the agents which provide the same external behaviour in any context. Since the universe of agents and the universe of contexts depend on the used action set, equality depends a priori on this set of actions. We show here that if we select from the universe of agents, two agents which are equal, they are also equal if we extend the universe of actions (and consequently if we extend the universe of agents and contexts).