[an error occurred while processing this directive]
���¿��ټ��� �߼�����
   ��ҳ  �ڿ�����  ��ί��  Ͷ��ָ��  �ڿ�����  ��������  �� �� ��  ��ϵ����
�������պ����ѧѧ�� 2007, Vol. 33 Issue (04) :472-476    DOI:
���� ����Ŀ¼ | ����Ŀ¼ | ������� | �߼����� << | >>
Ҧ����, ��ï��*
�������պ����ѧ �����ѧԺ, ���� 100083
Formal modeling and analysis of UML statecharts
Yao Shuzhen, Jing Maozhong*
School of Computer Science and Technology, Beijing University of Aeronautics and Astronautics, Beijing 100083, China

Download: PDF (0KB)   HTML 1KB   Export: BibTeX or EndNote (RIS)      Supporting Info
ժҪ Ϊ���״̬ͼ�Ľ�ģ����,�ر��Ǵ��и���״̬�IJ�λ�״̬ͼ�Ľ�ģ����,������UML״̬ͼ�Ľṹ�ص����������,�����˲�λ���ɫPetri��HCPN.������״̬��Petri�������ṹ���ֳ�����/����˿ڡ�״̬Ǩ�Ʋ��ֺ���ʷ״̬����.��������/����˿ڷֱ���������������뻡�Ľ������뿪�Ļ��Ļ���,״̬Ǩ�Ʋ������״̬�������ڲ�״̬�任,��ʷ״̬����ͨ��"���䵥Ԫ",��ɸ���״̬��"����ָ�"��"����ˢ��".�����������HCPN�ṹ,�ܽ���״̬ͼ����״̬ת��/ת��Ǩ�Ƶ������Լ������,�����˸���״̬��Petri����������Ӧ���������ͷ�������.������״̬ͼ�İ�ȫ��Ҫ����ϸ��������ʷ״̬�걸���ж�ԭ�򡢸��Ӳ�һ�����ж�ԭ���״̬�ɴ����ж�ԭ���HCPN�����ʾ.�о��ɹ��Խ�һ�������Զ���������֤����,�Ż�����ϵͳ��Ʒ���,����������������Ҫ��ָ������.
Email Alert
�ؼ����� ��ģ   Petri��   ����   ����     
Abstract�� The structural and semantic features of UML statecharts are analyzed firstly, and the hierarchical colored Petri net(HCPN) is constructed to solve modeling issues,especially those related to hierarchical statecharts with composite states. The Petri subnet for a composite state is composed of input/output interfaces, a state-transition part and a history state part. The input/output interfaces are used to parse entry arcs and gather exiting arcs to/from composites respectively. The state-transition part realizes transitions of the internal states. The history state part deals with memory recovery and memory cleanup of history units. After abstracting semantic rules and constrains of entry/exit transitions, their descriptions and analysis techniques of composite states based on HCPNs are illustrated. Finally, in the view of safety of UML statechart, HCPN semantic representation for completeness, consistency and reachability of statechart is elaborated. Optimizing the design of complex systems the guide in theory and practice for further research on developing automatic verification tools is provided.
Keywords�� model buildings   Petri nets   semantics   analysis     
Received 2006-12-15;
About author: Ҧ����(1965-),Ů,��������ľ˹��,����,szyao@buaa.edu.cn.
Ҧ����, ��ï��.UML״̬ͼ����ʽ����ģ�������[J]  �������պ����ѧѧ��, 2007,V33(04): 472-476
Yao Shuzhen, Jing Maozhong.Formal modeling and analysis of UML statecharts[J]  JOURNAL OF BEIJING UNIVERSITY OF AERONAUTICS AND A, 2007,V33(04): 472-476
http://bhxb.buaa.edu.cn//CN/     ��     http://bhxb.buaa.edu.cn//CN/Y2007/V33/I04/472
Copyright 2010 by �������պ����ѧѧ��