MOVIDA NCES Generator (MNG) is PLC source code, UML translator and Net Condition/Event (NCES) editor.

Having a model expressed in UML, one may translate it into TNCES by means of MOVIDA NCES Generator (MNG). MNG accepts models defined in XMI version 1.2. It has appeared that the Object Management Group (OMG) has defined an XMI format for the UML definition. XMI stands for XML Metadata Interchange. There are different versions of XMI defined and implemented by a majority of the UML tools available on the market.

The figure above demonstrates a framework of the tools that are used for system modeling and verification and validation. The Plant modeling is done with UML with a tool that supports the XMI export of the diagrams. XMI represents the diagrams in XML. At the same time, the controller source code may be developed and translated into TNCES by MNG. The MNG can input XMI file that holds a UML model and convert it into TNCES. Thus, we may get two models – model of the controller and model of the plant. The MNG is used to obtain models of the controller and the plant and interconnect them. The modules may be edited by the NCES Editor embedded into MNG.

The output of the MOVIDA NCES Generator can be introduced to verification tools developed by various authors. For example, it is possible to use integrated Model Assembler, Translator and CHecker (iMATCH) developed by Dr. Valeriy Vyatkin. The iMATCH has an integrated model-checker, which allows to verify simple logical propositions. The tool may also interface with SESA model checker developed at the University of Berlin.