The expanding smart distribution grid with gradually updating business modes is requiring a superior information model to reflect its state precisely. This paper proposed a formal modeling and verification method based on common information model. Considering the imprecision and ambiguity of UML in the modeling process, we constructed the formal definitions and logical descriptions for objects, logics and scenes of the information model, followed by the derivation of ontology rules and propositions. To verify whether the model possesses the expected semantic features, formal verification method is generalized using underlying logics and semantics derived from the ontology rules. Later on, the formal verification tool SPIN is applied to the distribution control area model as an example for formal verification to ensure the synchronization of semantics and structure for data exchange process between information models. a)The formal symbols in this paper adopt the following conventions: b)The formal expressions conform with Backus Naur form, BNF; c)The capital letters represent sets, lowercase letters denote the elements: t∊T; Definitions use the combination of numbers: 2–3; Rules use number and uppercase letter combination: 2-A; Inference use number and lowercase letter combination: 2-d
