Research On Runtime Verification For Software Behavior

With the wide application of software to telecommunication and finance, the scale of software systems is constantly expanding, and their structures and behaviors become more and more complicated. Therefore, people have more request and wish for their correctness, availability, reliability, safety, etc. Starting with an analysis of traditional quality controlling techniques like test and verification, and the features of runtime verification, this thesis presents the idea of runtime verification and analysis, with a focus on the pattern of software when it is running.Firstly, this thesis designs a language for describing behavior patterns after discussing the technique of describing software behavior, and provides the method that BPDL can automatically shift to Deterministic Finite Automaton (DFA). BPDL is a simple language, capable of making a formal description of software behavior traces while software is running. Meanwhile, it can also describe regulations of software behavior. BPDL is different from traditional description languages in that it views the complicated interactive behaviors among softwares as a series of events and behavior regulations, thus simplifying interactive behavior description, and bringing more convenience to runtime verification and analysis of software behavior.Secondly, based on a study of software runtime-verification techniques, this thesis presents a runtime verification framework, with a focus on software behavior. Within this framework, runtime verification is conducted at two levels. At the first level, the theory of DFA is adopted to check whether a single series of events conforms to behavior regulations or not. If behavior regulation violating occurs, the verification system gives some important attentions;Multi-Entity Bayesian Network(MEBN) technology is employed to verify and analyze complicated interactive behaviors, which are related to the past information. With the help of MEBN, the trustworthiness of on-going interactive entities can be automatically figured out, and then an immediate and objective judgment can be made, by combining real time experiences and past experiences of those entities. This framework allows flexible arrangement for interactive behavior monitoring. Verification and analysis can be conducted at two different levels, which can reduce software system performance influence, improve verification efficiency, and guarantee the correctness of verification and analysis.Lastly, this thesis implements the mechanism for software behavior running verification, and testifies it a typical prototypical system. It illustrates how to implement the core components in typical prototypical system, and makes simulation tests to verify and assess feasibility and efficiency of the runtime verification system.