Research On Inconsistency Verification Of Real--Time Safety Requirements Based On Natural Language

The quality of safety requirements is directly related to the success or failure of the system,and even the safety of people's life and property.With the increasing sys-tem scale,automated and accurate analysis of safety requirements is urgently required.Many safety standards recommend the use of formal methods,but now most companies still use natural language to express requirements.In order to bridge the gap between natural language and formalization and to deal with the low efficiency of existing ver-ification approaches based on formal methods,aiming at the real-time safety require-ments,this thesis proposes a real-time safety requirements pattern language(RTNL)to formally transform quasi natural language based requirements into formal language,and defines scalable algorithms to verify behavioral inconsistency,cyclic inconsistency and rt-inconsistency.The main contributions include:? RTNL is defined based on safety requirements pattern language(Safe NL).Thesyntax of simple patterns and compound pattern are given,and the semantics isprovided with Clock Constraint Specification Language(CCSL),so that the re-quirements in terms of quasi natural language can directly correspond to the formaldescription of CCSL.This laid the foundations for further analysis and verifica-tion.? The verification and location approaches for behavioral inconsistency and cyclicinconsistency of real-time safety requirements are defined.The behavioral in-consistency verification defines a set of common conflict patterns and providesan algorithm to directly filter out behavioral inconsistencies based on the conflictpattern.The cyclic inconsistency verification transforms the requirements intocausality clock graphs(CCGs),and thus reduces the verification into the a circulardependency search problem.And then based on the circular dependency detectedin CCG,the least inconsistent requirement set is located,and an algorithm is de-signed to explain the occurrence of cyclic inconsistency.? The verification and location approach for rt-inconsistency of real-time safety re-quirements are defined.The approach transforms the real-time safety require-ments into real-time clock graphs(RCGs),and reduces the verification into agraph computation problem.It designs an automatic verification algorithm for rt-inconsistency,and locates the least inconsistent requirements set in terms of RTNLbased on the verification result.At last,the supporting tool Requirements Consistency Verifier of above approaches is implemented.Real cases from the industry are used to verify the validity of our approaches.Efficiency,and scalability are evaluated through a set of experiments.The results show the efficiency of the proposed approaches and can be used to verify large number requirements.