The IEC 61499 standard establishes a framework specifically designed for the implementation of decentralized reconfigurable industrial automation systems. However, the process of distributed system's validation and verification is difficult and error-prone. This paper discusses the needs of model generators which are capable of automatically translating IEC 61499 function blocks into formal models following specific execution semantics. In particular, this paper introduces the prototype Net Condition/Event Systems model generator and aims to summarize the generic techniques of model translation.