Analysis And Verification Of UML Diagrams Based On Formal Method

Model Driven Development?MDD?focuses on the intensive use of models during software development.In this paradigm,models are the central artifact for software development.With MDD,the models can be transformed to derive executable programs and to derive tests.This makes building quality models a cost-effective software development approach,as the models can be reused for many analysis or generation goals,and not just document a design.However,to successfully developing software with MDD,high quality models are needed.Hence,performance analysis of high-level behavioral specifications,such as UML,is needed to enhance their qualities,detect defects,and ensure desired behavior.The UML2.0 behavioral models are used in understanding and communicating the problem domain concepts,during the analysis and design phase of the system.The absence of formal semantics for UML behavioral models makes it difficult to build automated tools for their analysis,simulation and validation.It seems obvious that the complexity of model analysis and model design contributes to errors and a lack of understanding to the users and system analysts alike.Coloured Petri Nets?CPN?is well known for describing distributed and concurrent complex systems.Furthermore,numerous techniques,e.g.,simulation,testing,state space-based techniques,structural methods and model checking,are currently available for analyzing CPN models.Therefore,to design models in the form of CPN,by integrating all scenarios into a coherent whole and fitting for further detailed design,is promising for performance verification and validation of CPN modules.For these reasons,CPN was chosen as the formalization method.Additionally,the software CPN-Tools was applied for modeling the system structure and analyzing its performance.CPN-Tools is a software for editing,simulating,and analyzing CPN models.Various stochastic scenarios can be simulated in the model.It can be set to follow different stochastic distributions to monitor real situations.For more analysis,converting CPN models to MXML and then applying various process mining techniques and tools can give more results about the system.Process mining techniques target the automatic discovery of information about process models,which is based on the execution data recorded in MXML event logs.The aim of this thesis is to conduct formal analysis,validation,and verification of the UML2.0 model activity diagram related to the use case description by means of Colored Petri Nets?CPN?.Firstly,the UML models semantics were defined.These semantics were formalized into Coloured Petri Nets?CPN?.Secondly,the CPN model correctness was validated using the state space analysis and simulation-based verification techniques by means of CPN-Tools.Thirdly,the corresponding checking queries codes were developed with SML language for the purpose of model safety verification of deadlock,safety,liveness,etc.Fourthly,the analysis results of the properties of the CPN models were generated in the form of the state space reports,and performance analysis depending on simulation by means of monitors in CPN-Tools was used to assemble data in Log files and generate simulation reports.Finally,process-mining techniques were applied to an ATM transaction dataset obtained and selected randomly.We pre-process this dataset,the resulted CPN model from the transformation of UML 2.0 use case can be converted to MXML by using ProM_import framework.The process mining technology by using ProM5.2 was applied to prove the validation and safety functions of the ATM system.The state space analysis was used to calculate the properties results such as?Liveness,Home,Boundedness,and Statistics?which were generated in the form of the report.In conclusion,firstly from the state space analysis results,it was shown that there are no deadlocks,safety,livelocks,and dead marking using different checking queries.From model checking?ASK-CTL?,it proved that the system works accurately and no inconsistencies were observed by using some of the propriety written as a form in CTL.Furthermore,based on the process-mining results,it was noticed that the customers frequently use only some ATM operations.Specifically,Insert card,Enter PIN,Select Withdrawal,Use Authorize,Enter Amount,Check Balance.In addition,it also has proven that the CPN use case ATM system is similarly identical with ATM in bank.By using formal method,especially CPN,the analysis,validation,and verification of UML Diagrams are highly efficient and easily to implement.The software process conversion techniques are very important to assist in acclimatizing the rapidly varying desires of users.