Research Of Requirement Model Check Based On Multi-View And SoftWare Behavior

With the incredible development of computer science and technology, software system is becoming more and more complex, thus requiring more and more strict requirement on its quality. One of a critical step to decide the final quality of software system is the software requirement analyse step, which is also called software requirement engineering(RE). RE focuses on the technology that uses engineered methodology to describe and analyse software requirements, in order to gain a high quality requirements. Thus, may cover two aspect:the describing of requirements and then verify it. The describing of requirements is to combine documents and requirements model to precisely record the function, capability and constraints that the target system should have. The latter one is then analysing the completeness, soundness, feasibility and validity of requirements. These two aspects connects as well as important.Along with the development of RE, some new concepts has been proposed. In the requirements analyse of complex system, it is inevitably that various of participants that with different background, knowledge and responsibility would be refered. This indeed causes the development of RE on multi-view points. Multi-view points RE applies different view points to gain and organize different requirements and opinions of different participants, in order to construct the final system requirements. However, lots of unsolved problems still stays in this field. Such as:1) How to construct the requirements document based on multi view points.2) How to discovery the inconsistent in the documents.3) How to construct requirements model formally.4) How to formally analyse the requirements model.To the forenamed three, the department i studyed in have done a lot of research, and proposed a formal language called BDL(Behavior Descriptive Language), to describe requirements based on multi-view points. The key idea of BDL is to apply software behavior to describe scene that would shows in runtime, and every view point is established by a series of interactive scenarios. In this thesis, we mainly focuses on the formal analyse of validity of requirements based on multi-veiw points and software behavior model(behavior model for short). To be more precise, we would follow the traditional three steps to do our work:behavior model construction, properties construction and check whether the model satisfy our properties. To be more clearly, the main contribution of this thesis is as follows:1) Modeling methodology:We simply introduce the process to construct behavior model, and analyse the basic principles of our methodology.2) Modeling language:We introduce the basic syntax of modeling language:BDL, and discuss about its semantics. The basic BDL elements and operators are mapped into an abstract algebra called behavior algebra, and define the states of model evolution. The dynamic run of behavior model is interpreted as states transition.3) Properties describing:We analyse the relationship between system properties and requirements, and proposed a describing language based on branching time, for which we called BTL(Behavior Temporal Logic). We argue that by the use of properties pattern, we would have a more improvement on the soundness, readability and reusability on properties design.4) Checking methodology:We treat this part into two different situations:the function related properties and quality related properties. To the former one, we first translate behavior model into a states transition system, and generate interpretations of properties on the system to judge whether the model satisfy the propertits. Besides, we discuss about the optimize approaches for the sake of states explosion with the help of the characteristic of behavior model from compositional deduction and proposition abstract. In the quality check, we use the exponential distribution of atomic behavior execution delay and markov properties that the model demonstrates during evolution to simulate the situation the runtime situation of system, and analyse the quality properties such as rate of resource utilize, throughput of critical services,etc.5) Case study:Finally we give a software project called "Book Shop On Line" to demonstrate our work. We first model the system with BDL and then validate some properties of it, we also give a precise analyse of the whole process.