董威，王戟，齐治昌.UML statecharts的切片模型检验方法[J].电子学报, 2002, 30(12): 2084-2089. ？DONG Wei, WANG Ji, QI Zhichang. Slicing UML statecharts for model checking[J]. Acta Electronica Sinica, 2002, 30(12): 2084-2089.？
[2]
李留英，王戟，齐治昌.UML Statechart图的操作语义[J].软件学报,2001,12(12): 1864-1873. ？LI Liuying , WANG Ji, QI Zhichang. An operational semantics for UML statechart diagrams[J]. Journal of Software, 2003, 14(4): 750-756.？
[3]
周颖，郑国梁，李宣东.面向模型检验的UML状态机语义[J].电子学报, 2002,30(12):2091-2095. ？ZHOU Ying, ZHENG Guoliang, LI Xuandong. An operational semantics for UML state machines in model checking context[J]. Acta Electronica Sinica, 2002, 30(12): 2091-2095.？
[4]
MROWKA R, SZMUC T. UML statecharts compositional semantics in lotos[C]// International Symposium on Parallel and Distributed Computing.[s.l.], 2008:459-463.？
[5]
PRASHANTH C M, SHET K C, ELAMKULAM J. Verification framework for detecting safety violations in UML statecharts[C]//Second Asia International Conference on Modelling & Simulation. [s.l.], 2008:849-854.？
[6]
CHENG Liang, ZHANG Yang. A verification method of security model based on UML and model checking[J]. Chinese Journal of Computers, 2009, 32(4):699-708.
[7]
LIANG P,AVGERIOU P, CLERC V. Requirements reasoning for distributed requirements analysis using semantic wiki[C]// Fourth IEEE International Conference on Global Software Engineering.[s.l.], 2009： 388-393.？
[8]
OGAWA H, KUMENO F, HONIDEN S. Model checking process with goal oriented requirements analysis[C]// 15th Asia-Pacific Software Engineering Conference, 2008. Beijing, 2008： 377-384.？
[9]
BAIER C, KATOEN J P, LARSEN K G. Principles of model checking [M]. Cambridge：The MIT Press, 2008：1-30.
[10]
CLARKE E M, GRUMBERG O, PELED D A. Model checking[M].Cambridge: The MIT Press，1999：26-30.？
[11]
MIKK E, LAKHNECH Y, PETERSOHN C, SIEGEL M. On formal semantics of statecharts as supported by STATEMATE[C]// Proceedings of the 2nd BCS-FACS Northern Formal Methods Workshop. London: Springer-Verlag, 1997:68-82.？
[12]
董威，王戟，齐治昌.UML Statecharts的模型检验方法[J].软件学报, 2003, 14(4): 750-756. ？DONG Wei, WANG Ji, QI Zhichang. An approach of model checking UML statecharts[J]. Journal of Software, 2003, 14(4): 750-756.？
[13]
YAO S, SHATZ S M. Consistency checking of UML dynamic models based on petri net techniques[C]// 15th International Conference on Computing.[s.l.], 2006: 289-297.？
[14]
CLARKE E M,HEINLE W. Modular translation of statecharts to SMV, Technical Report CMU-CS-00-XXX[R].[s.l.]. Carnegie-Mellon University of Computer Science, 2000.？
