Formal Verification of Smart System Based on Hierarchical Combination Abstract
ZHOU Yilong
HAN Bin
Abstract：In this paper,a formal modeling and verification method is proposed for the smart system. Firstly the system is di?vided into application layer,system layer and equipment layer by hierarchical thought. Based on the system functional requirements and hardware module,the Kripke structure model of each layer is built. Then,the hierarchical model is combined according to the combination model rules,and the combination abstract model of system is obtained after abstraction processing. Finally,taking the energy sharing system as an example,the system model with CSP# is described,the system property with LTL is described,and PAT tool is used to complete the automatic verification of the system model. The results show that the proposed method considers the behavior of each subject in system. It can effectively find out the design flaws in the smart system and can alleviate the problem of state space explosion in model checking.
Keywords：formal methodsmart systemcombination abstract modelmodel checking
Publication Date：2019-01-01
Online Publishing Date：2025-08-15(First online date of this platform, not the publication date of the document)
Pages：5( 1917-1920,1984 )