Abstract:A conceptual model of the command and control object (C2O) is described using the formal language LOTOS(Language of Temporal Ordering Specification), and the main properties of C2O and C2O-based systems are defined using ACTL(Action Based Temporal Logical). Then a model-based-verification approach is provided aiming at the above key properties verification. The practical example shows that the new approach is viable.