39 results about "Timed automaton" patented technology

The invention relates to the technical field of industrial control system network flow detection, and aims to provide an industrial control network abnormal behavior detection method based on a trusted model. According to the method, on the basis of fully analyzing the network flow of the industrial control system, a detection model is established based on a timed automaton algorithm. Through analysis, the network data packet transmitted by adopting the industrial control protocol has the characteristics that the control channel is fixed, the length of the data packet is fixed, the data packetstate machine is fixed, and the transmitted data packet conforms to a certain time rule. In the detection process, once a strange channel, a strange data packet type and a data packet which does notconform to time constraint appear, an alarm is given. The method is different from a traditional detection method based on signatures and white lists, the characteristic vector of the time dimension is introduced, and higher-level attack behaviors can be detected. The invention provides a new solution for detecting the abnormal behavior in the industrial control system.

The invention provides a CPS modeling and property verification method based on a possibility space-time hybrid automaton. The verification method comprises the steps that 1, the possibility space-time hybrid automaton and a cyber-physical system (CPS) are determined; 2, the properties of the possibility space-time CPS are verified. The method is based on a possibility space-time hybrid automaton model and used for modeling of the CPS, a description language of the possibility space-time CPS is given to be used for verifying and measuring system responsiveness, regular security and other properties, the effectiveness of the CPS modeling and property verification and measurement method in an uncertain environment is verified in terms of theory and instance, and a theoretical basis is provided for intelligent control and optimization of the complicated CPS.

The invention presents a real-time testing system and testing method based on the time safe in-out automaton which is a modification of time automaton. The method firstly converts the system model expressed by time safe in-out automaton to stable symbol state transition graph without abstract time delay and lift; the variable transition action sequence which contains time delay and fulfills various structures covering standard is generated statically by the testing method of input/output grade lifting system; at last, the time delay variable is resolved dynamically with introduced time extreme value function and linear constrained-solution method to test. The testing system with the method suits for various black box tests with software system which is restrained by time.

The invention relates to a car-following behavior generation method based on a timed automaton. The car-following behavior generation method comprises the steps of: S1, extracting car-following data from a traffic data set, regarding a rear car speed, a relative distance and a relative speed between a rear car and a front car as input parameters of a car-following model, and symbolizing the input parameters; S2, training the car-following model by utilizing a timed automaton learning algorithm to obtain a car-following model automaton; S3, regarding a hidden state of the car-following model automaton as substates of following cars, clustering the substates for representing car-following sub-behaviors; S4, establishing a Helly car-following model for each car-following sub-behavior, and carrying out parameter calibration on each Helly car-following model to obtain rear car acceleration under the corresponding sub-behavior, thereby acquiring a car-following trajectory. Compared with the prior art, the car-following behavior generation method is used for learning symbols by means of the timed automaton to obtain the hidden state, clustering the substates to represent the sub-behaviors of the following cars better, shows the human car-following behavior trajectory precisely, and improves the intelligent level of unmanned vehicles.

The invention provides an evaluation and detection system of the robustness of a network system, and an operating method of the evaluation and detection system. According to the evaluation and detection system, firstly, a timed automaton of a protocol of the network system is constructed, and an overall working process of the protocol is described; secondly, weighted migration is introduced into a model for expanding the timed automaton; and lastly, a random timed automaton of the network system is constructed for modeling of uncertain factors in the environment. On the basis of the random timed automaton, statistical model testing technology can be used for analysis and evaluation of the performance of the network system, and therefore the objects of parameter configuration, performance comparison and the like are achieved in a design stage and a selection stage of the protocol. According to the operating method of the evaluation and detection system, the performance of the network system in a specific environment is analyzed and evaluated mainly through the modeling of the protocol and the environment in the unstable network system, and therefore the robustness of the network system is evaluated and detected. The statistical model testing technology is based on a simulation and statistical method, and therefore an exhaustive search of the state of the network system is avoided, consumption in time and space is greatly lowered, and the statistical model testing technology can be used for processing a large-scale system.

The invention discloses a model verification method based on a source code. The method comprises the steps of obtaining a target source code; modeling the target source code according to an AADL modeling technology to generate an AADL model; converting the AADL model into a time automaton model based on a preset conversion mode; and checking the time automaton model by using a preset model detector. Therefore, by adopting the embodiment of the invention, the verification efficiency can be improved.

A system for testing functionalities of a vehicle while driving the vehicle having a message-based bus network topology comprises a software server configured to be connected to the bus and to take vehicle sub-system information therefrom and interpret it as output from a timed automaton. The system also comprises at least one client in the form of an executable test script written in a programming language and configured to from the server subscribe specific vehicle sub-system information to be used by a test assessment oracle of the test script for assessing a particular function or sub-function of the vehicle.

The invention discloses an ultrafiltration flow rate timed automatic mechanical flushing valve device, which comprises a mechanical flushing valve arranged on an ultrafiltration membrane flushing water pipeline, wherein the tail end of a valve rod of the mechanical flushing valve is fixedly connected with a driving device, the driving device is arranged and assembled in an ultrafiltration membrane clean water outlet pipeline, the driving device drives the valve rod to rotate through the impact mechanical rotation via water flow flowing in the ultrafiltration membrane clean water outlet pipeline, the mechanical flushing valve is provided with a mechanical flushing valve diaphragm group sheathed and matched with the valve rod, the mechanical flushing valve diaphragm group is respectively provided with an upper flushing water guide hole, a lower flushing water guide hole and a middle connecting passage, the middle connecting passage is used for communicating the upper flushing water guide hole and the lower flushing water guide hole, and the driving device drives the middle connecting passage to do circumferential rotation through the valve rod under the impact effect of the water flow to realize the periodic on-off states of the upper flushing water guide hole and the lower flushing water guide hole, so the on-off state of the ultrafiltration membrane flushing water pipeline is controlled, and the timed flushing opening and closing function of the flow rate type mechanical transmission is realized.

The invention relates to a domain name matching method based on a tree automaton. The method comprises the following steps: filling a domain name to be matched and each fragment of a model substring to integer multiples of n bytes, wherein n is equal to L divided by 8 and L is a minimum operation bit width of a computer system; then constructing the tree automaton by taking the n bytes of the model substring as units; then, sequentially executing the tree automaton of the domain name to be matched until a domain name matching is finished from a root node. By taking the n bytes as the matching units when a matching operation is carried out, the matching operation efficiency of the method is much higher than that of an existing character string matching method; the tree automaton takes a hash value as a table item storage address, and a storage space occupied by table items can be reduced; a hash collision domain is limited in a local-grade node. The domain name matching method based on the tree automaton is applicable to fixed prefix matching or fixed postfix matching of the domain name, and the matching operation of other character strings with same stratification characteristics.

The invention discloses a task schedulability verification method for a distributed system. The task schedulability verification method comprises the following steps: 1, simulating the distributed system by adopting a processor model based on a timed automaton model, a task model, a scheduling model and a network bus model; wherein the task model sets a task in a ready state after the task is issued, and adjusts the state of the task according to the scheduling of the scheduling model and the attribute of the task; the scheduling model schedules the task to the processor model or the network bus model according to a scheduling rule; the processor model or the network bus model carries out switching between an idle state and an occupied state according to a processor or a bus simulated by the processor model or the network bus model after receiving the tasks distributed by the scheduling model; and 2, verifying and analyzing whether the task is completed at the deadline time, the occupation condition of the bus and the occupation condition of the processor by means of a simulation analysis tool so as to judge the task schedulability of the distributed system.

The invention discloses a conversion tool and method from a model B to a timed automaton network. The tool includes an Event-B metamodel, a time automaton network metamodel, an EventB2NTA model transformation engine and an EventB2NTA model transformation configuration module. The method includes: combining and storing the Context model of the buc format of the Event-B and the Machine model of thebum format into an Event-B model of the xmi format; and converting the preprocessed Event-B model of the xmi format into the time automaton network model of the xmi format; storing the time automatonnetwork model in the xmi format as an xml format recognizable by the time automaton network tool UPPAAL, and then adding the corresponding time attribute according to the user's requirements to complete the modeling. The tool can be integrated into the Eclipse platform, and combines the advantages of the gradual refinement of the Event-B model with the explicit characterization of the time characteristics of the time automaton network model.

The invention discloses a reverse-osmosis flow timing automatic mechanical flushing valve device which comprises a mechanical flushing valve. The mechanical flushing valve is connected with an energy conversion driving mechanism, and the energy conversion driving mechanism comprises an energy converter provided with a conversion output shaft, wherein the water inlet end of the energy converter is connected with a water drain pipe opening of a reverse-osmosis membrane filter element, and a first water outlet pipeline of the energy converter is connected with a waste water pool. The tail portion of the conversion output shaft is arranged in a central installing hole of the mechanical flushing valve in a penetrating mode, the mechanical flushing valve is provided with an axial flushing water guide hole connected with a second water outlet of the energy converter, an axial flushing water hole channel and a middle connecting channel, the energy converter converts potential energy produced by flushing water flow discharged by the reverse-osmosis membrane filter element into mechanical energy for driving the conversion output shaft to rotate, and the conversion output shaft drives the middle connecting channel of the mechanical flushing valve to perform rotary movement, thereby achieving periodical communication and non-communication between the axial flushing water guide hole and the axial flushing water hole channel and achieving the purpose of cleaning control through flow timing.

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.