How to perform the composability checking between models is one crucial issue in the composable simulation development. In light of this, the reference model of composability checking problem was proposed，then an approach to semantic representation of simulation models based on Hoare Logic was presented. As the compatibility and substitutability are the two flip sides of composability coin, the rules to check the compatibility and substitutability between semantics of simulation models were constructed, and the formal approach to semantic composability checking was established. Finally, the relations between the semantic compatibility and substitutability were analyzed.