Science & Engineering Research Support soCiety (SERSC)
UML has become the de facto standard software modeling language. It includes use case diagrams, class diagrams, activity diagrams and state chart diagrams. Semantics of UML state chart diagrams and timed automata are represented by timed transition systems. Based on the semantic equivalence, a method for transforming a state chart diagram into timed automata is proposed for the purpose of formally verifying requirements specification described by simplified CTL (Computation Tree Logic). The timed automata and simplified CTL is used as inputs of Uppaal for model checking.