- Li Tan, Zongyuan Yang, and Jinkui Xie. "UCVSC: A Formal Approach to UML Class Diagram Online Verification Based on Situation Calculus", in Proceedings of the 4th International Conference on Computer Sciences and Convergence Information Technology (ICCIT'09), pp. 375-380, Seoul, Korea, Nov. 2009.
The gap between informal models used in a UML environment and formal verifications and proofs in academic research prevents UML from valid and efficient application. In this paper, we propose an approach to bridge the gap between UML class diagram and situation calculus via our formal verification tool, UCVSC (UML Class diagram online Verification based on Situation Calculus). UML class diagram describes a software system informally while situation calculus is employed as the underlying formalism to precisely specify the system. With respect to most components in UML class diagram, the strength of reasoning about actions and describing the state of the world in situation calculus can be applied to represent them appropriately. Using UML tools and predefined mapping mechanism, we transform UML class diagram to XMI, an intermediate format, and finally to situation calculus in Prolog syntax. This approach attempts to provide precise semantics of UML class diagram which can be logically verified. In addition, we automate the verification process in an online prototype system. Furthermore, a case study on an academic system is presented to illustrate and evaluate our approach.
- Li Tan, Zongyuan Yang, and Jinkui Xie. "OCL Constraints Automatic Generation for UML Class Diagram", in Proceedings of the International Conference on Software Engineering and Service Science (ICSESS’10), pp. 392-395, Beijing, China, July 2010.
As a standard modeling language of software architecture design, UML lacks formal semantics on account of its informal graphical notation. To further provide refined description of UML, OCL is primarily and widely employed. Generally, OCL constraints are written manually, which may cause incorrectness and extra overhead. Therefore, generating OCL constraints template for UML models is a superior solution. The OCL constraints template automatically generated can be used as a reference for software designers. First of all, the significance of automatic generation of OCL constraints was emphasized, and then the application domain of OCL was shown, followed by a lexical analysis of how to extract the target objects in UML models where OCL constraints were needed to build and an algorithm of extraction. Eventually, this extraction algorithm was implemented by Perl. In our way, the overall quality and efficiency of software design is enhanced and thus contributions are made for the automation of Software Engineering.
- Li Tan, Zongyuan Yang, and Jinkui Xie. "Verifying UML in Prolog", submitted.
From the viewpoint of software life cycle in Software Engineering, software architecture is the core of the structure and behavior of software. As software architecture design itself is a kind of modeling activity, how to verify the correctness of the standard modeling language of software architecture design, UML, is one big problem. This paper used the implementation of situation calculus, Prolog, to describe a subset of UML diagrams, a graphic notation formally and evaluate it an equivalent formal semantics. Then we verified possible syntax and semantic errors in UML in a Prolog interpreter, SWI-Prolog, after a definition of error types in UML. Finally, a goal was achieved that software designers could correct the design of UML diagrams prior to fixing bugs in code in the phase of test, which avoided unnecessary system overhead in the following phases of Software Engineering with the hope of enhancing the overall efficiency of the process of Software Engineering.