Description And Refinement Of The Bank ATM System Based On UML And Temporal Logic Language

Software architecture has emerged as a hot spot in the international software engineering fields in the 1990s. With the size and complexity of software system increasing, the design of architecture has always been a major factor in determining the success of systems.Software architecture description is a chiefly research task. Now the main methods of software architecture description are visual description and formal description. They have complementary advantages in describing software architecture. The method of visual description can describe system distinctly, UML is typical of visual description.UML provides a whole set of concepts and graphical method which can describe software system. However, UML lacks of precise semantics, so that it is difficult to analyze the models strictly. The method of formal description can describe system precisely, for example XYZ/E. XYZ/E is a executable temporal logic language. It can express systems'description of different abstraction levels from formal criterion to executable programs in a uniform temporal logic frame. This characteristic is suitable to description, refinement and design of software architecture.This paper discusses how to describe software architecture by combining UML and XYZ/E. Firstly it discusses the feasibility of combining UML and XYZ/E. All kinds of diagram of UML are suitable to describe different systems structures and behaviors, but they lack same semantics basis so that they can't express the inherent relation of system. XYZ/E is very suitable as rationale of the formal method, but the support to the concept of software architecture is still not enough. According to consideration of the aspect, we enlarge the wording composition of XYZ/E and make it support the basic concept of software architecture on the language.We extend and constraint the elements of UML, then define XYZ/E semantics of UML activity diagram, so they can describe software architecture in a better way. At last, the feasibility of this method is explained further by the description and refinement of a bank ATM system's architecture.The research of this paper will promote the research of software architecture description, formal semantics of UML and the appliance of formal methods in the software development etc.