Building A Cloud-based Application Software Model Using UML And Event-B

Unified modeling language(UML) pervades the practices of software engineering.UML is a set of techniques as well as a sort of modeling language.UML is so-called a semi-formal language. On one hand, the abstract syntaxes of UML constructs are described by formal language, but the semantics of UML constructs are portrayed by nature language. This is one reason to classify it as a semi-formal language. And on the other hand, UML technique doesn't specify how to formally verify a model by itself though it can depict the model formally. This is another reason to say UML is a semi-formal language. In practice, the formal part of UML is capable of depicting things precisely, while the non-formal part of UML makes itself to be understood or mastered more easily. But there are still some scenarios are beyond UML's capabilities. One of these scenarios is to analyze the inconsistencies of models before and after evolution.The evolution of UML models from phase to phase would introduce the inconsistency problems. Exploiting formal methods is a way to analyze the inconsistency problems of UML models. Event-B is a set of formal techniques which can do this job. Event-B can formally depict models as well as verify them. The cardinal work of this dissertation is going to develop a method of integrating UML technique with Event-B technique. Firstly, this dissertation provides a process to define the rules for transforming a UML model to an Event-B model and the transforming algorithms, and defines a conformance standard for these transforming algorithms. And a set of concrete transforming algorithms are provided, whose conformance is proved as well.Secondly,it's presented that the semantics of models before and after transformation are consistent; therefore the equivalence of these models is proved consequently. Thirdly anintegrated method to formally analyze the inconsistency of UML models is provided. Finally, this integration method is applied to a cloud-based application software model.Briefly, the contents of this dissertation include:Firstly analyze the pros and cons of semi-formal UML. And introduce the progress to overcome its cons. Point out a new solution which is going to combine Event-B and UML will be introduced in this dissertation.Secondly introduce the UML technique, including the meta-meta-model of UML, the meta-model of UMLand the unified develop process with UML. Introduce the Event-B technique, including the meta-meta model of Event-B, the meta-model of Event-B, and the Rodin platform of Event-B.Thirdly develop a method to transform UML models to Event-B models. Present that the semantics of models before and after transformation are consistent; consequently prove the equivalence of these models.Fourthly develop an integrated method to analyze inconsistencies of UML models before and after evolution. Present how to use this method by a case study.Lastly build a cloud-based application software model. And apply this integrated method to this model so as to improve the model.Theapplication of this integrated method shows the effectiveness of itself. This method is valid and effective for analyzer and designer to improve the quality of models in software engineering early phases.