The Functionalities Checking And Non-functionalities Measuring Of Software System Based On UML

As the software systems becoming larger and more complex, the more are expected from the software, more concerns are put at checking software methods and measuring system performance. Since based on UML (Unified Modeling Language) software design methods has become an industry standard, it's an a good solution to get some requirement and performance information from UML for analyzing and finding system's potential bugs and performance bottlenecks.UML is a general-purpose, object-oriented, visual modeling language with the advantages of intuitive modeling, easy to understand, convenient for the presentation and usage, automatically code generating. However, UML lacks of precise formal description. The Petri net is formal language which can be used to describe the dynamic behavior, and it particularity describe concurrent and distribution systems.In this paper, we fully integrated the two modeling languages-UML and Petri net, which can complement to each others, on the one hand we can design the software intuitively, on the other hand, we can also describe the dynamic behavior of the software. First, we describe the system with UML, then we translate the UML state diagrams with non-functional information into Petri net model, Based on the Petri net, we check functionalities and measure non-functionalities.In the functionalities checking, we filter out the non-functional information from Petri net, and then transform the Petri net to PROMEL an input language of the model checking tool SPIN. We denote the functions to be checked by linear temporal logic (LTL) formula. By analyzing the running results and the execution traces of SPIN, we determine if the functions are satisfied by the system.When the non-functionalities measuring of the system, we translate the Petri net to stochastic Petri net, since any continuous time SPN with finite places and transitions is isomorphic to a one-dimensional continuous time Markov chain(CTMC), so based on Markov chain model, we obtained the mathematics formulas tocalculate the feasibility, safety, performance efficiency of the system.Finally, a Service Robot example has been used to illustrate our method.