The Research Of Runtime Verification Technology Based On Live Sequence Chart

With the development of computer technology, reliability of software systems attracts more and more attention. Especially for safety-critical systems, how to improve the reliability of such systems has become a very important research direction. Traditional test method can be used to protect the reliability of software systems, but it has incompleteness problem. Model checking is a completeness method, but it requires abstract modeling system, and for complex systems, model checking easily lead "state space explosion" issues. Runtime verification technology is an effective complement to traditional methods, it can help to improve the reliability of software system. Runtime verification concerns the actual execution of software system meets the requirements specification to be verified. Using visual requirements description language modeling requirements specification scene is a hotspot in runtime verification. Currentlty, Runtime verification technology of visual scene-based requirements specification has the following disadvantages:(1) Existing verification methods easily generated redundant properties, verification overhead is quite large and the two true value semantics verification result is not accurate.(2) The efficiency of existing runtime verification algorithm of rewriting logic based on Maude is low, it is not conducive to rapid discovery of a system failure.For the inadequacies of existing runtime verification technology, the contributions are:(1) Analysis the inadequacies of existing verification method, an improved runtime verification method based on live sequence chart is proposed. The method uses code instrumentation to get system execution trace, uses live sequence chart to describe system requirements specification. To support existing runtime verification technologies, the form of requirements specification is converted from live sequence chart into LTL formulas, then use the transitivity of properties in live sequence chart to simplify scale of resulting LTL formula. Then based on the three-valued logic LTL finite trace executable semantics and rewriting logic runtime monitoring algorithm to realize runtime verification.(2) For the efficiency of existing runtime verification algorithm of rewriting logic based on Maude is low, according to Maude features, this thesis uses the idea of status consumption, introducing the caching mechanism of operators to improve efficiency of formula rewriting, in order to quickly find the system failure.(3) Design verification tools and complete experimental examples to prove the feasibility of the proposed method. Based on above research, this thesis has developed a verification tool RVT4LSC. Using RVT4LSC to verify the RBC/RBC handover scenario of ETCS-2 train control system, experiment results demonstrate the feasibility of the proposed method. The comparative experiments are carried out, experimental results show that, conversion method used in this paper will have a smaller scale LTL formulas, the proposed method can effectively reduce the overhead of runtime verification.