From graphical representations to formal specifications and return: translation algorithms in the Harmony environment

We introduce the translation algorithms that support the combination of semiformal graphical representations with formal notations in the Harmony environment for software specification. Background information is presented about the Harmony approach and details of both formalization and deformalization processes are provided. Even though the algorithms described are focused on UML to Z++ translations, their underlying principles and rules can be adapted and reused for other combinations of modeling notations, in particular for combinations that involve UML for the graphical representation of software models. Several directions of enhancing the existing translation algorithms are also discussed.