| Modern software systems have tremendous impact on society and human lives; however, developing reliable software remains challenging. Through mathematically provable specifications, formal methods make it possible for designers to describe, ver-ify, and validate systems in a rigorous way. The use of formal methods is motivated by the expectation that performing appropriate mathematical analyses of software behav-iors can lead to improved reliability of a design. Model-driven engineering (MDE) is a mainstream software development methodology with models used as artifacts driving the development. In MDE, the focus is on practical usability of specification languages, analysis methods, and tools. Unified Modeling Language (UML) is an important part of MDE and has become the de facto standard for modeling. However, it is hard to perform formal verification on models due to the lack of precise formal semantics for UML. More importantly, the design of software is usually an incremental iterative re-finement process. Unfortunately, there do not exist widely-adopted specifications of the refinement relation between UML models, let alone practical tools that can auto-mate the process. As a result, it is extremely difficult to ensure that a model correctly refines its predecessor.The work described in this thesis develops techniques across formal methods and MDE, making contributions in both fields. In particular, we explore the idea of using the state-of-the-art theorem proof assistant Coq to formalize and mechanize the seman-tics for UML dynamic diagrams as well as the refinement relation between models. Through an automated metamodeling-level conversion tool, the entire UML semantic-s can be expressed as definitions in Coq, which are often referred to as mechanized semantics. Based on mechanized semantics, desired properties of both the UML se-mantics and the refinement relation can be stated as lemmas. The proof of each lemma ensures the satisfaction of these properties. We can also verify, mechanically, whether models conform to the refinement relation. In order to improve the reliability of the incremental software development process, a framework of machine-checkable refine-ment of software design models has been proposed. The main contributions of this thesis can be summarized as follows:● We demonstrate how to implement the mechanized semantics for UML sequence diagrams and state diagrams and perform formal verification in Coq. Recent years have witnessing a significant progress in formal software verification us-ing mechanized semantics. For example, much effort has been made to use Coq to formally describe the semantics for various kinds of system software (such as compilers, operating systems, relational databases, etc.) and prove their correct-ness. As a part of the UML dynamic behavior diagram family, UML sequence diagrams and state diagrams are the core diagrams to specify the behavior of software. The state-of-the-art research focuses mostly on UML static models (especially the class diagrams), not on dynamic models. In this thesis, we target this important problem of formally modeling and verifying dynamic diagrams. In particular, we represent the syntax of UML sequence diagrams and state dia-grams as inductive types, and the denotational semantics for sequence diagrams and the operational semantics for state diagrams as inductive predicates. By do-ing so, we can use the higher-order logic system in Coq to do inductive reasoning on the structure of UML models. The denotational semantics for sequence dia-grams covers mostly-used interaction operators. The operational semantics for state diagrams supports characteristic features such as entry/exit actions, history mechanism, inter-level transitions and priority judgment, etc. Based on mecha-nized semantics, the desired properties on models can be stated as lemmas and the proofs of lemmas ensure their correctness.● We propose a formalism for specifying the refinement relation between UML se-quence diagram models and between UML state diagram models, which enables us to prove important properties of the refinement relation in Coq. Refinement serves as the basis for the incremental design and development process. While refinement is well-defined in the literature of formal specification languages, as a semi-formal specification language, UML does not directly support refinement mechanisms with proof of correction. The lack of the refinement support makes it difficult to ensure that a UML model correctly refines its predecessor. Hence, it is highly desirable to formalize the refinement relation so that its correctness can be formally verified. By using inductive predicates in Coq, we implement the refinement relation and mechanically prove that the refinement relation be-tween UML sequence diagrams is reflexive, transitive, and context insensitive. We also prove, mechanically, that the refinement relation on UML state dia-grams is reflexive, transitive, and behavioral preservative. Transitivity implies that the correctness of a multi-step refinement can be checked by verifying the correctness of each individual refinement step. Context insensitivity implies that a sequence diagram can be compositionally refined. Behavioral preservation implies that when a state diagram is refined, it adds new functionality without changing existing behaviors.● We propose a framework of machine-checkable refinement of software design models. With the help of an automated transformation tool, one can formally analyze systems, verify desirable properties of design models, and whether a UML model correctly refines its predecessor. The framework is highly flexi-ble and scalable, providing increased reliability guarantee for future design and implementation of large-scale, complex software systems. Using Kermeta (a metamodeling language) and predefined transformation rules that are directly added to the meta-model of UML diagrams, models of UML diagrams can be automatically transformed into Coq code. This tool provides useful additional support for the proposed verification framework. |
PDF Full Text Request