����Petri��B/S��ϵ�ܹ�����������ϵͳ��ģ����֤
������1 ,����1 ,�¶�2
1. ������ѧ
Modeling and verification of online judge system with B/S based on Petri nets
ժҪ ��������ϵͳ���Կ������绷���£�ʵ�ֶ�̬�������һ���д���Ե�ϵͳ����Դ�ͳ�������ƽ�ģ�������Ѽ��ϵͳ��̬�ṹ�������Ͷ�̬��Ϊ�ķ���������P/T����һ��B/S�ܹ�����������ϵͳ���ģ�͡����ϵͳ���ܣ�����˱�֤ϵͳ������ȷ��Ӧ���е���Ҫ���ʣ��̶���S_��������������˷�������֤��
�ؼ�� ��
Petri�� ,
�������� ,
B/S�ܹ� ,
P/Tϵͳ ,
S_������
Abstract ��Online judge system is a representative system in dynamic transaction processing under network environment. The properties of static structure and dynamic behavior were not considered by the conventional design method of software. A hierarchical model of online judge with B/S was constructed by P/T nets. According to the function, some important qualities were presented to guarantee the correctness of system. The analysis and verification of the model are shown by S_invariants.
Key words ��
Petri net
online judge
Browser/Server ��B/S�� architecture
Place/Transition net
S_invariant
�ո�����: 2009-04-16
��������: 2009-10-28
�������: ���������ӵ�Petri��Ľṹ�����о�
ͨѶ����:
������
E-mail: xhu_chenxl@163.com
[1]
��ƽ ������ �Ͻ�. Ŀ���֪�¼���Ļ��е���ͻ���Ʋ���
[2]
������ ���ξ�. �����ƶ�Agent���ƶ��Ƽ���ϵͳ��������
[3]
������ ���� ��Զ��. ����Լ���Ż���Petri��ɴ��Է���
[4]
������ ���� ����. ����Petri����п�ϵͳ��ʽ����������
[5]
Ī��ƽ ������ ������ ����. �����ƻ�Petri��ı��Ա任
[6]
��ʽ�� ����Խ. ������Petri���Web�����ģ��
[7]
��� ʷ��ɽ ���˽�. ����Petri��Ľ��蹤����Ŀʵʩ�ι�������ģ�����
[8]
�ƹ��� ������ �ű�. ������չʱ�����Petri��Ĵֲ����繥��ģ��
[9]
�Ʋ��� ������ ������ Ī��ƽ. Petri������Ķ�̬�����о�
[10]
������ ������ �Ž�. �ദ���������㷨ʵ�ּ���Petri��ģ�����
[11]
������ �ƹ���. ���ڴֲڱ�Ҷ˹���ĵ����繥������
[12]
������ �ƹ���. ���ڴ����Թ���ģ�͵�������в����
[13]
���� ���Ŀ� ������ ������ ��ɺ. ���ڶ�Agent��Ӧ��ЭͬPetri��ģ��Эͬ���
[14]
���� ������ ������ ֣��. Java���������ݴ�ģ�ͷ���������
[15]
������ ���� ��ѩ��. ���ߴ���������ģ�͵���ʽ����ģ���������
2009, Vol. 29 
