Research On Verification And Correction Of Time Properties Of UML Interaction Models

Software design plays an increasingly important role in Software Life Cycle.Reasonable and effective design will make the subsequent development process more stable and correct.The earlier the software problem is discovered,the lower the repair cost is,which means that it is especially important to verify the software design.On the one hand,the UML interaction model consisting of UML interaction overview diagram and UML sequence diagram is a common system interaction scenario modeling language in software design.It can intuitively describe the interactive behavior of the system.On the other hand,time is one of the important properties of the interaction system.Therefore,this thesis focuses on the time-property verification of the UML interaction model and how to correct the time constraints when time-property is not satisfied.The verification of the time-property of the UML interaction model belongs to the category of model checking.One of the ideas of model checking is to calculate all the state space of the system at one time,but there is the disadvantage of state space explosion,and the calculation volume is large and the efficiency is low.This thesis decomposes the entire model checking into a way to test each bounded path,which reduces the complexity and state space of a single verification,and improves inspection efficiency.At the same time,the time constraints will be corrected when the time-property in the bounded path is not satisfied.The main work of this thesis addresses the following aspects:·A bounded reachability verification method for UML interaction model based on SAT-LP-IIS is proposed.First of all,in this thesis,Boolean Satisfiability Problem(SAT)is adopted to encode the UML interaction model as a conjunctive normal form,then bounded paths will be found by finding the normal form solution.Next,for the time constraints in the path,Linear Programming(LP)is applied to check whether the time constraint is satisfied.The time constraints in UML interaction model are all linear constraints,which can be quickly solved by using LP technology.Then,when the UML interaction model is very large,the Irreducible Infeasible Subset(IIS)is adopted in this thesis to accelerate the processing.For infeasible paths,IIS technology could find the smallest infeasible path segment.All the paths that contain the smallest infeasible path segment are infeasible paths.These infeasible paths can be abandoned,which greatly improves the efficiency of processing.·For unsatisfactory time constraints,it may mean that there are design flaws in the UML interaction model.We have proposed a correction proposal to make unsatisfied time constraints become satisfied time constraints by correcting IIS.