The Research And Application Of Agile Software Development Process Based On Formal Methods

In this thesis,the software decomposition method and the agile development process are formalized by the mathematical concepts such as vector,set and Cartesian Product,then the formal model of agile development process is proposed which is used in software quality assurance.With the help of the theory of differential dynamical system,it is proved that the defect can't be eliminated,which proves that the formal model is of some theoretical value.The main work of this thesis is as follows:Firstly,software is a complex system,and it must be decomposed to developing.Choosing the data flow diagram to study the software decomposition method due to the data flow diagram is a typical structured analysis method.The semi-formal model which is represented by class diagram is proposed by using the data flow diagram to analyze the software decomposition process.The formal model of software decomposition is proposed and the dependency relationship between functions is deduced by using the mathematical concepts such as vector,set and Cartesian Product to formalize the data in the data flow diagram and using function to formalize the process in the data flow diagram.Secondly,the traditional development process such as waterfall model,rapid prototyping model and incremental model is studied by using business process model,and the Scrum in agile development process is studied emphatically.The semi-formal model of Scrum is abstracted by analyzing the Scrum development process by business process model and analyzing the Scrum artifacts and their dependency relationship by class diagram in which the middle process of the black box is added.Combining the semi-formal of software decomposition and Scrum,the correspondence between the process in the data flow diagram and Scrum artifacts and intermediate products in the Scrum development process is discussed.The formal model of Scrum artifacts is proposed and the dependency relationship between Scrum artifacts is deduced by using concepts in the formal model of software decomposition.Thirdly,according to the formal model of software decomposition and Scrum artifacts,the definition of concepts such as tasks,error in software development process and concepts such as defect,software status in software.The formal model of agile development process is proposed and deducing the error propagation route in development process and the route that errors cause defect.Fourth,the defect propagation model is constructed by applying the formal model into software quality assurance.Analyzing the defect propagation model through the stability theory,and it is obtained that the unique equilibrium of the defect propagation model is global asymptotically stable which proves that defects can't be eliminated.Thus,the conclusion that the formal model is of some theoretical value is proved.