This paper presents PLCTools, a formal environment for designing and simulating programmable controllers. Control models are specified with IEC FBD (Function Block Diagram), and translated into functionally equivalent HLTPNs (High-Level Timed Petri Nets), through MetaEnv, for analysis and simulation and obtained results are presented in terms of suitable animations of FBD blocks. The peculiarity with FBD is that it does not come with a fixed set of syntactic elements; it allows users to add as many new blocks as they want. Consequently, each time users want to add a new FBD block with PLCTools, they must provide the concrete syntax, to add it to the library of available blocks, but also the associated HLTPN, to allow MetaEnv to build the formal representation.