Environment Model Based Requirements Consistency Verification

Nowadays formal methods have shown their power in requirements consistency verification,especially for safety-critical systems.However,most of the existing re-quirements verification researches only focus on the software requirements specifica-tion,without considering the interactive environment of software,and the verification efficiency is not high.In this thesis,along the line of environment modeling based requirements engineering,we extend the environmental properties to the scope of re-quirements specification verification,and propose an environment model based light-weight approach for the requirements consistency verification.Specifically,we extract environment property constraints from the interactive scenarios and state transitions of environment entities,and transform them into a formal model in the form of a clock graph.On this basis,we reduce the consistency verification problem to the traversal problem of the clock graph.The main contributions of this thesis include:? The environment model is extended to the scope of requirements consistency ver-ification emphasizing the role of the environment model in the consistency veri-fication of the software requirements specification,,put it into the requirements specification to be verified,and environment properties are taken as inherent con-straints that must be satisfied.? A formal representation method of the environment model and the requirement models is presented.A set of transformation rules are defined.They directly trans-form the internal state transitions of environment entities and interactive scenarios into formal CCSL(Clock Constraint Specification Language)constraints,laying a solid foundation for subsequent analysis and verification.? A light-weight requirement consistency verification method based on the clock graph is defined.It composes the clock graphs from different scenarios and state diagrams together,removes some unnecessary clock and clock constraints by sim-plifying the clock graph,then orchestrates inconsistent scenario based on simpli-fied clock graph and visualizes the orchestrated inconsistent scenario.In order to support this method,we implement an environment model based re-quirements consistency verification tool(Env-Consistency),and apply it on industrial cases.To highlight the advantages of this method,this thesis designs several compar-ative experiments to evaluate the proposed method.The evaluation results show the effectiveness and efficiency of our method,and also proof the effects of environment properties in the requirements consistency verification.