Formal Modeling And Application Research Of System Based On Model Checking

In the application process of computer system,in order to avoid the losses caused by minor errors,before these systems are put into use,they need to be modeled according to the system properties and analyze and verify the built models to ensure that the system functions is robustness before the system is put into use.Model checking is a formal verification method based on mathematics,which provides convenience for property verification,system development,system modification and maintenance of computer systems.This paper studies model checking methods and related theories,and applies them to the formal modeling and attribute verification of the system.Compared with the general real-time system,it is a kind of computer control system with the highest performance for the security of the system.This system includes discrete behavior generally and also contains continuous behavior with time constraints.In the process of system development and modeling,the current popular modeling method is to use the semi-formal unified modeling language UML and timed automaton with time elements to model.The main contributions of this article include the following aspects:(1)The computer railway station interlocking system is very demanding for the security of the system.This paper studies the establishment of the sub module of the basic route in the system,and proposes a formal modeling method based on the analysis of multiple UML combination scenarios.Firstly,the method uses pre-condition and post-condition analysis methods of OCL to analyze multiple combined UML time sequence scenarios,checks the contradictory behaviors in the scene and resolves the contradictions,and obtains a consistent multi-combination UML time sequence scenario,and then it will be consistent.The behavior sequence of the object interaction in the scene is transformed into a finite state process algebra model,and the combination operation is performed in the model detection tool to obtain a formalized model of the system.This method provides a new idea for the requirement analysis and design research of security critical system software,and provides a better solution for the formal modeling and verification analysis of the system based on scene analysis.(2)This paper proposes a modeling method for Internet of Things system composite services based on the theory of timed automata.In the fourth chapter of this paper,based on the atomic services of the Internet of Things,it simultaneously performs the traditional timed automata.Some extensions are used to apply the extended timed automata model to the layered modeling of IoT(nternet of Things)atomic service modeling and composite services.According to the analysis of atomic individual attributes in atomic services,tools named UPPAAL are used to perform the model construction.Validation analysis.This article stands at a microscopic point of view to analyze and model individual individuals in the system.Then from a macroscopic point of view,individual individuals are linked together by relevance to make it a complete system.It is necessary to grasp the individual Uniqueness also needs to grasp the overall connectivity.Through the research of this paper,according to different systems,analyzing the property requirements of different systems,targeted modeling,improve the accuracy of system modeling,and reduce the software development and maintenance costs.Through research examples,we can know that the proposed method has a good practical significance.