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.