Interpretation, Transformation and Model Checking of Semi-formal Diagram Notations

Thanks to their intuition and directness, semi-formal graph notations, such as UML, FBD and ER-diagram, have been widely used in every stage of software development to compose a comprehensive specification. But on the other hand, because of the lack of precise definition of semantic, it results in some problems, for example, the inconsistencies of those notations are very difficult to be checked and to be integrated. In order to settle those problems, this paper presents an approach based on graph transformation and epistemic logic to interpret, transform and model checking those semi-formal notations. By this way, we can preserve the merits of semi-formal notations and at the same time enhance the requirement specification´s quality.