Pattern Languages And Pattern Templates For Runtime Verification

As a lightweight formal verification method,runtime verification has been applied in many fields,for instance Java program runtime verification,hardware runtime verification,and train control system runtime verification.Among all advantages of using formal specification in runtime verification,the most prominent one is that a class of errors about monitored objects can be specified exactly.Meanwhile,there are two drawbacks in existing methods of describing formal specifications in runtime verification.Firstly,only constants are used to describe events,which limits the descriptive scope of specifications.Secondly,constructing formal specifications asks for strong professional background,which affects the promotion and usage of runtime verification.Therefore,it has theoretical significance and application value to study a new formal specification and present corresponding algorithms for runtime verification.In this article,some researches has been conducted,to address the problem mentioned above.Specifically,the main innovations are as follows:1.To make up the first drawback,we put forward the formal definitions of pattern and pattern language,and introduce theories of pattern language into the runtime verification.We also present the application of pattern matching in runtime verification.2.To make up the second drawback,we propose pattern templates and pattern library to simplify the design process of formal specification.First of all,in order to handle runtime verification problems in offline monitoring,we put forward and implement Brute Force extended algorithm,Boyer-Moore extended algorithm and Sunday extended algorithm.In order to handle runtime verification problems in online monitoring,we put forward and implement the pattern matching algrorithms.And then,by simulating runtime verification,the experimental results show that the Sunday extended algorithm,pattern templates with HashMap structure and specifying relational pattern templates have better performance on efficiency than others.Besides,we propose the Accepted State Automata and the pattern inference algorithm to enhance the expressive power of pattern templates.3.According to extending the runtime verification tool Monitor Verification Control,we design and implement the functions of verification for pattern language and pattern templates.Furthermore,we verify the validity of the formal definitions and algorithms in engineering.Above all,pattern language can enforce the descriptive power of specification,as well as simplify the transformation process from natural language specification to corresponding formal specification,by calling pattern templates in pattern library.In this way,not only can it reduce the design of specification in runtime verification,but also lower the threshold of constructing the formal specifications.