The paper contributes some formal techniques for the system modeling development discussed in [1]. Based on a kind of multi-sorted first order logic, the language CML is used to specify system models conceptually, and the analyser CMA is followed to check their static consistency and dynamic temporal.