Research On Methodology Of Requirements Tracing Based Onpredicate Logic

The embedded software has been widely used in safety-critical areas such as aerospace, nuclear energy and transportation, it is extremely vital to ensure its safety. Maintaining the traceability between software artifacts during the software development process is an important challenge for software safety.Current research on traceability has two main problems. On one hand, it mainly focuses on the traceability between requirements and source code or design and source code, there is a lack of research about traceability between requirements or between requirements and design. On the other hand, traceability information built by major ways such as the recovery of trace relations based on information retrieval has low accuracy and completeness, it usually can't be effectively applied in the development of software in safety-critical areas.To solve these problems, this thesis proposes a semantic model for the traceability information between requirements and design based on predicate logic. Based on the semantic model, trace relations can be automatically inferred and checked, and the accuracy and completeness of relations can be guaranteed. The major work is listed as follows.Firstly, a semantic model for requirements tracing is built. we design a symbolic system based on predicate logic to describe the traceability information between software artifacts. And then, semantics of relation types between requirements such as dependency, refine, decompose and conflict is given. Besides, we define the semantics of relation type between requirements and design.Secondly, methods for automatically inferring and checking of trace relations are given based on the semantic model. We propose rules for inference and consistency checking by analyzing the semantics of requirements relations, and the algorithms for automatic inferring and checking are designed. In addition, based on the semantics of traces, constrains for the satisfy relations between requirements and statecharts are given, which support partially inference and check of the satisfy relations.Finally, a prototype tool is designed and implemented based on the method we proposed.It supports the modeling of traceability information between software artifacts and the analysis of trace relations. The effectiveness and feasibility of proposed method is demonstrated through a case study.