Formal Verification Studies On Integrating Problem Frames And UML

In the information age,software products have become important and indispensable in our real life.As a carrier of the information exchanges and automatic control of production,software gradually plays an important role in the development of human society.With software being widely used,software products have become inseparable from our lives,such as daily online chat,enter-tainment,shopping,national military and aerospaces.On the one hand,we are enjoying all kinds of convenient services that software products bring to us;on the other hand,we may suffer from financial loss and even accidental personal damages because of software defects or failures.In addition,some large-scale software-intensive project delays can cause huge loss in manpower and financial resources.There may many reasons for these problems,such as the device failures or hardware malfunctions,improper manual operation etc.,but one of the most important reasons is software requirements.Software requirements analysis is the starting point and foundation of the whole software development.It also provides an important basis for software testing in later phases of software development.Therefore,the study of software requirements engineering has become an integral part of the software development and maintenance,and it is of important theoretical significance and practical significance.The problem-oriented approach to software requirements analysis,namely the Problem Frames approach(PF),provides a wider perspective and a meaningful reference model to build a solution to the software development problem.PF emphasizes the correct understanding of the problem that exists in the real world before looking for the solutions prematurely.Problem-ori-ented software development is derived from PF.In the early phase of software requirements anal-ysis,our focus should be on the problem,rather than the solution.The problem diagram is an instance of problem framework model,which consists of the computing machine,the real world domains and the requirements.Software specifications describe the behavior of the computing machine when interacting with adjacent application domains.Requirements are behavior descrip-tions of application domains prescribed by the customers.In PF,software requirements are satis-fied by the overall behaviors of the machine and the problem domains.The work in this dissertation is focused mainly on the formal semantics of Problem Frames.In other words,we verify whether there is a solution to the problem diagram model,and verify whether the solution meets the requirements.This dissertation integrates PF and UML(UnifiedModeling Language),and proposes a formal verification process,which consists of six steps.The static aspect of the problem diagram model is mapped to a UML class diagram,which can then be checked by the UML4PF tool(the plug-in runs in Eclipse platform)to test the completeness and correctness of our UML diagram model.After establishing a complete and correct problem dia-gram model,we designed a searching algorithm for causal chains in a problem diagram.which can then help the identification of a causal chain in the diagram.If such a causal chain is found,we can hypothesize that there is a possible solution to the problem.The dynamic aspect of problem diagram model are mapped to UML statecharts in order to verify whether the specification S,to-gether with knowledge about the context K,satisfies the requirement R.Then we establish the one-to-one mapping relationship between the statechart diagram and the CSP(Communicating Se-quential Processes)notation.So the specification S,requirement R and context K are all described in CSP,Finally,with the help of some popular model checking tools such PAT or FDR,we can check whether the CSP specification model refines the requirement model.In this dissertation,the two kinds of verifications,namely verifying the static behavior and dynamic behavior of the prob-lem diagram model,enable us to correct the error of the software requirement analysis model in early phase of software development,which ensures we get a high quality requirements model.In this way,we can avoid the spreading of errors to subsequent software development stages,thus saving unnecessary costs at the same time.