Generating method of temporal automata model combining pac learning theory and active learning

Abstract

The invention provides a method for generating a timed automata model combining PAC learning theory and active learning, which is used to generate a single-clock timed automata formal model of a real-time system. Observation table; step S2, process the time observation table through the converter to meet the closure and consistency; step S3, based on the time observation table, construct the hypothetical model through the learner step S4, compare the quality of the hypothetical model with the stable model through the comparator quality, and judge whether a counterexample is found; step S5, when the judgment in step 4 is no, conduct a PAC approximate equivalent query on the hypothetical model through the teaching device, and judge whether a counterexample is found, when the judgment is no, stop the iteration, and assume The model is used as the result model; step S6, when step S4 or step S5 judges yes, update the time observation table according to the counterexample, and return to step S2.

Description

technical field [0001] The invention belongs to the technical field of software development, in particular to a method for generating a time automaton model combining PAC learning theory and active learning, which is used to generate a deterministic single-clock time automata formal model of a real-time system. Background technique [0002] With the rapid development of real-time embedded systems, the reliability and security of the system have received more and more attention from industry and governments. At present, the inspection of the system is mainly realized by technologies such as model-based testing and formal verification. Formal models are a prerequisite for the application of these technologies, but in reality, it is generally difficult to directly obtain formal models due to problems such as legacy software, missing documentation, inaccessible or incomprehensible source code. Model learning is a method of automatically modeling a system through its input and o...

AI Technical Summary

Problems solved by technology

However, at present, there is still little work on model learning for real-time systems, especially active learning. The above-mentioned libraries and tools are mainly concentrated on systems without time information, and the learned formal models lack the description of system time information. However, For some real-time systems with strict time constraints, a time-related error may often cause significant losses. When analyzing and verifying these real-time systems, time is an indispensable dimension, so the above tools cannot be used to such real-time embedded systems

Images