Formal Verification of a UML State Chart Diagram with Uppaal
Nianhua Yang, Guo Xin-shun, Wenjie Wang · 2012
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, CTL). The timed automata and simplified CTL is used as inputs of Uppaal for model checking.