The Research Of Runtime Verification Technology Based On Timed Sequence Diagram

With the wide application of information technology, computer technology has been widely used in various fields. However, computer system’s exception may result in disastrous consequences.The test and simulation are often used to ensure the reliability of this kind of safety critical systems, but the method is used for the system before the actual operation, can only detect system error, and can not prove that the system is correct. Model verification is complete, can explain the correctness of system, but it is for the abstract model of the system, it is difficult to prove the equivalence of the abstract model and the actual system, at the same time, this method requires all execution paths traverse system, for the complex systems, easy to produce the problem of combination explosion.Runtime verification is an effective complement to the traditional method such as teach model test and verification techniques, it is for the actual running system. Runtime verification generally uses temporal logic to describe the requirement specifications to be verified and constructs monitors on the basis of requirement specifications. However, it is difficult for those software engineers who do not have any formal experience to use temporal logic to describe the requirement specifications due to the complexities of temporal logic and formal methods. Sequence diagrams are commonly used to describe the requirement specifications, and they have been widely used in the industrial areas. So the research of generating monitors automatically based on the timed property sequence diagram becomes meaningful.This paper proposes a method to generate monitors automatically based on the U ML2.0timed property sequence diagram. The specific idea is using the sequence diagr am to describe the requirement specifications to be verified, then constructing the time d automaton for each object in the sequence diagram, transforming the entire sequence diagram into timed automaton network.Firstly,this paper presents the time sequence di agram formal definition of property to meet the requirements of the verification of the paper, then it presents the basic principle of authentication method based on the time s equence diagram property,and thus giving the structure prediction monitor algorithm t hat is transforming the time sequence diagram property into the timed automatic Netw ork. On this basis, this paper firstly performed functional tests:Constructing a verifica tion tool named TPSD_monitor based on the sequence diagram using the above princip le, then constructing a simulation system and using the tool to validate the constructed simulation system to prove the feasibility of the method, finally conducting performanc e comparison tests. Experimental results show that this method can effectively describe the requirement specifications to be verified and it is easy for the software engineers la cking formal experience to master because generating monitors and running them is of small overhead. It can meet validation requirements for real-time and concurrency, and it can also effectively relieve combinatorial explosion during the generation process of the monitors.