Formal Analysis And Verification Of Energy Sharing System Based On Hierarchical Combination Abstract

With the development of computer software and hardware technology,the performance of hardware and software systems has been greatly improved.Systems become more and more complex,at the same time,it is easier to go wrong.Compared with the traditional technology like simulation and test,formal method has the basis of strict mathematical theory,so it can describe and model the system accurately.Then model detection technology can be used to verify if the system meets the property requirement.The verify progress has the characteristics of high credibility and automation.Therefore,formal method has been widely used in the design and development of hardware and software systems.However,as the coverage area of the system becoming larger,the scale of software and hardware is expanding,and the system is characterized by high concurrency.The problem of state space explosion often occurs in the process of model detection.The paper adjusts and combines the combination method and abstract method after studying them.At the same time,by introducing the idea of hierarchy,a method of modeling and verification based on hierarchical combination abstract is given.The method can layered model the system according to its characteristics,aimed at finding defects in the system design in time,and reducing the problem of state space explosion in detection by reducing the system redundancy state.The main contribution of the paper is as follows:(1)The rules of classical combination and abstract method are extended,and the formal method of modeling and verification for complex systems is given: By introducing the idea of hierarchy,the system is divided into multi-level based on the characteristics then modeled,and the system hierarchy model is described with Kripke structure.By defining the combination rules between the hierarchical models and the abstract rules of the hierarchical combination model,the Kripke structure model of each layer is combined and abstracted,and the hierarchical combination abstract model of the system is obtained.Then the Kripke structure is transformed into the CSP#(Communication Sequential Process Sharp)model,and the corresponding verification strategy is formulated.(2)Taking the energy sharing system as an example,the structure of the energy sharing system is analyzed and modeled.The hierarchical structure of the system is defined in a formal way,which facilitates the analysis of the input and output relations between various layers of the system,and lays a theoretical foundation for the establishment of the system model and the formal specification of the system.(3)The formal specification of the system model is carried out by the formal language CSP#,and the Linear Temporal Logic LTL(linear time series logic)is used to describe the property which system needs to meet.PAT(Process Analysis Toolkit)tool is used to automatically check the system model,and to find out the defects of the system then improve it.The results of experiment show that the method can effectively solve the problem of state space explosion in model checking while finding out the design defects in the energy sharing system.