Real-time method for verification of protocol using check of region model

摘要

This invention specifies the requirements in the form of time automata (1) in the development of real-time protocol and demonstrates the integrity and completeness of the specification in a real-time verification method that confirms before implementation whether the timed automaton specification model conforms to the requirements. In order to provide a method of using a regional model test, the real-time protocol verification method (13) applying the regional model test is based on the regional model graph based on the specification model of temporal automata (1) and the temporal mue calculation logic (8). (9) uses the real-time local model inspection algorithm (14), which performs real-time verification by focusing only on the logical value of the initial node of the local product graph, and the time automata specification model is a logical formula of the temporal mue calculation method. Using the real-time safety verification method (15) to check whether the expressed real-time safety characteristic (30) is satisfied Real-time to check the existence of a temporal livelock that does not return to the initial state of the real-time protocol model by repeating infinitely only a subset of temporal deadlocks or states that do not cause a transition due to lack of logical and temporal accuracy in the temporal automata specification model. Performs safety verification and checks whether the time automata specification model satisfies the real-time necessity characteristics expressed by the logical expression of the temporal mue calculation method, using a real-time necessity verification method (16) within an arbitrary time after an action occurs in the time automata specification model. Real-time necessity verification is performed to confirm that the desired behavior occurs.