Based on Formal Methods in Trustable Software Requirements Engineering

In order to strengthen the reliability of software and improve the efficiency of software development, this paper proposes a formal methodology for software requirements engineering and designs a model which consists of MZASR (Model based on Z language to analysis software requirements) and MZMSR (Model based on Z language to management software requirements) to implement the software requirements management and maintain. First of all, we describe the software requirements specification by UML tools and models, which are divided into three-level where individual semantics are specified as Z-specification by approach bottom-up. Meanwhile, we refine every specification step by step for obtaining richer software requirements. Secondly, when talk about how to verify the result of the changed requirements, the process chains that composed by the Z-specification schemas interaction are used to check the changed software requirements for consistency with the help of the process algebra method. By analyzing the execution paths, we can know whether the affect of requirements update meet user´s original need or not. Finally, the experiments show that our approach is an improved method.