PLCTOOLS: design, formal validation, and code generation for programmable controllers

Strong timing requirements and complex interactions with controlled elements complicate the design and validation of software controllers. Different techniques have been proposed to cope with these problems during the different development steps: for example, differential equations for modeling controlled elements, the IEC 1131-3 notations for designing the software controller, and formal models for validating the design, but no definitive solutions have been proposed yet. The paper describes PLCTOOLS, a toolbox that exploits all the aforementioned techniques to supply an integrated environment for the design, formal validation, and automatic code generation of software controllers