The Formalization of UML State Chart with the Temporal Description Logics

UML state chart is lack of dynamic and temporal semantics defined strictly, so it is difficult to implement formal analysis and verification on the systems described by it. Description Logics (DLs), a formal language of knowledge representations, has very strong ability of representation and deduction, but the traditional DLs can only represent the knowledge about static application domains. Temporal logics (TLs) makes representation and reasoning about dynamic models more concise than using formalism such as pure DLs. TDLs (temporal description logics), the combination of DLs and TLs, can express both the dynamic and temporal semantics. So, we combine the advantages of DLs and TLs, a novel formalization of UML state chart with TDLs is proposed in this paper. Example indicates that the method is feasible, the semantic accuracy and expression ability of UML state chart are improved.