[an error occurred while processing this directive]
   
 
���¿��ټ��� �߼�����
   ��ҳ  �ڿ�����  ��ί��  Ͷ��ָ��  �ڿ�����  ��������  �� �� ��  ��ϵ����
�������պ����ѧѧ�� 2012, Vol. 38 Issue (1) :64-68,105    DOI:
���� ����Ŀ¼ | ����Ŀ¼ | ������� | �߼����� << | >>
������չPetri���ij��������ȫ����ģ����֤
����, ����, ½����, ������*
�������պ����ѧ �ɿ�����ϵͳ����ѧԺ, ���� 100191
Modeling and verification of de-icing software safety requirement based on expanded Petri net
Li Zhen, Liu Bin, Lu Minyan, Yin Yongfeng*
School of Reliability and Systems Engineering, Beijing University of Aeronautics and Astronautics, Beijing 100191, China

ժҪ
�����
�������
Download: PDF (669KB)   HTML 1KB   Export: BibTeX or EndNote (RIS)      Supporting Info
ժҪ Petri������ʽ����ϵͳ��ģ����,���ϸ����ѧ��������֤ϵͳ����ȷ����,����֧�ָ��������ģ���Զ�����֤������ڲ���.��չ��Petri������ʽ����,��������״̬�ͺ���ֵ�Ϳ���,�������˱�Ǩ�ļ���������״̬,��������ǰ�á�һԪ������жϹ���,ͬʱ������ʽ�����彫ģ���Զ�ת��Ϊ�������ʵʩ��ȫ����֤.�����������Ϸ����ڵ��Ͱ�ȫ�ؼ����-����ϵͳ�ϵ�Ӧ��,���̺ͽ��������չ��ģ�ͺͷ�����ǿ��Petri���Ը������ϵͳ�Ľ�ģ����,���������İ�ȫ��,��ģ�͵���֤������Զ�ת�����������ģ��ʱ�˹��޸���Ӧ����Ĺ���������˶�������Ϊ������ظ�������������.
Service
�ѱ����Ƽ�������
�����ҵ����
�������ù�����
Email Alert
RSS
�����������
�ؼ����� �����ȫ��   �������   Petri��   ģ�ͼ���     
Abstract�� As a formal method, Petri net can ensure the correct construction of system but lacks the ability of modeling complicated system and automatic verification. Firstly, the formal semantics of Petri net was expanded, the place of state and numeric were distinctively defined, the transition state of fired and inhibitory were distinctively defined, the non-precondition, unitary precondition and composite precondition were introduced, and the model was transformed into verification program to implement the safety verification according to formal definitions. And then, the effectiveness of this methodology was illustrated with an application in an aircraft de-icing system which is a typical safety-critical system. The process and result show that the expanded model and methodology enhance the ability of Petri net to model complicated software system, improve the software safety, and the automatic transform from model to codes settle the workload of rewrite corresponding code manually and the meaningless faults introduced by that when the model should be modified.
Keywords�� software safety   software engineering   Petri net   model checking     
Received 2010-05-14;
Fund:

"ʮһ��"�ص�Ԥ�п���(51319070101); ���տ�ѧ����������Ŀ(20095551025); ������Ȼ��ѧ����������Ŀ(70971056); ����������̻��о�ר��(DY09Z11926)

About author: �� ��(1977-),��,�����˻���,��ʿ��,��Ϊ���տƼ���ѧ������ϢѧԺ��ʦ,justlz@163.com.
���ñ���:   
����, ����, ½����, ������.������չPetri���ij��������ȫ����ģ����֤[J]  �������պ����ѧѧ��, 2012,V38(1): 64-68,105
Li Zhen, Liu Bin, Lu Minyan, Yin Yongfeng.Modeling and verification of de-icing software safety requirement based on expanded Petri net[J]  JOURNAL OF BEIJING UNIVERSITY OF AERONAUTICS AND A, 2012,V38(1): 64-68,105
���ӱ���:  
http://bhxb.buaa.edu.cn//CN/     ��     http://bhxb.buaa.edu.cn//CN/Y2012/V38/I1/64
Copyright 2010 by �������պ����ѧѧ��