Consistency Checking Of Graphic Models

Graphic models are widely used in both research and practice of software engineering thanks to their intuitive and expressive features. Consistency is an important property about models'quality, especially in model-driven development where models are the main artefacts of software development. Great efforts have been made on checking graphic models'consistency in the past decade. Due to the informal nature of graphic modelling languages, however, existing proposals are mostly based on empirical rules. This thesis proposes an approach to checking graphical models'consistency based on the solid foundation of the formal definitions of the abstract syntax and semantics of modelling languages. The approach is demonstrated with an object-oriented modelling language UML and an agent-oriented modelling language CAMLE. A prototype tool supporting the formalisation and analysis of models was implemented.The research addresses three related aspects: formal specification of consistency constraints, validation of consistency constraints, and evaluation of consistency checking methods.Consistency constraints serve as the criteria for evaluating models'consistency. Formally specified consistency constraints provide the base for validating the constraints, developing consistency checking tools and testing the tools. This thesis proposes a method for systematically deriving first order constraint language from abstract syntax of modelling languages. By constraint language, we mean a language for specifying consistency constraints. Two techniques of deriving constraint languages are developed addressing two different ways of abstract syntax specification of graphic modelling languages, including textual abstract syntax in GEBFN (Graphically Extended BNF), and metamodel in UML class diagrams.Correctly defined consistency constraints reveal part of the semantics of a modelling language. However, how to validate the correctness of consistency constraints with respect to the semantics of a modelling language remains an open problem. The thesis proposes to establish the semantic foundation of consistency constraints by formalising the semantics of modelling languages in first order logic. Seeing a graphic modelling language as a specification language, we represent the semantics of a model with a set of first order statements about the modelled system. The semantics of a metamodel is expressed as a set of first order statements that must be satisfied by all models, hence called axioms of models. The correctness of consistency constraints can be validated through formally proving their logical consistency with the axioms. Moreover, the consistency of a metamodel or a model can be analysed through formally proving the logical consistency of the logic system representing its semantics. A prototype tool LAMBDES (Logic Analyser of Models/Metamodels Based on DEscriptive Semantics) was implemented to translate metamodels and models into first order logic systems and to analyse them through logical inference.Due to the computational complexity, to check models'consistency by logical inference is less efficient than by specially designed consistency checking tools that implements a set of consistency constraints. How to evaluate such tools in terms of their effectiveness in detecting errors in models is also an open problem. The thesis proposes a data mutation testing method for testing consistency checking tools and evaluating consistency checking methods. In data mutation testing, a set of data mutation operators is designed to imitate various types of errors that may occur during modelling. By applying the data mutation operators on a few correct models, a large amount of mutants which contain all possible inconsistencies can be generated as test cases for a consistency checker. A case study of the method in the testing of CAMLE consistency checker is reported.