Efficient verification of a class of time Petri nets using linear programming

被引：1
作者：
Li, XD
Lilius, J
机构：
[1] Abo Akad Univ, Dept Comp Sci, Turku Ctr Comp Sci, TUCS, FIN-20520 Turku, Finland
[2] Nanjing Univ, Dept COmp Sci & Technol, State Key Lab Novel Software Technol, Nanjing 210093, Jiangsu, Peoples R China
来源：
INFORMATION PROCESSING LETTERS | 2001年 / 77卷 / 5-6期
基金：
中国国家自然科学基金;
关键词：
real-time systems; model-checking; duration calculus; concurrency;
D O I：
10.1016/S0020-0190(00)00156-3
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
An method that is based on the investigation of the untimed state-space of the underlying time Petri net is presented. This method avoids the need to deal with the timing constraints at each step explicitly. Instead, it uses linear programming to check the runs in timed state space corresponding to a path in the untime state space, but apply this step only when needed.
引用
收藏
页码：219 / 224
页数：6
相关论文
共 9 条
[1]   Computing accumulated delays in real-time systems [J].
Alur, R ;
Courcoubetis, C ;
Henzinger, TA .
FORMAL METHODS IN SYSTEM DESIGN, 1997, 11 (02) :137-155
[2]   MODELING AND VERIFICATION OF TIME-DEPENDENT SYSTEMS USING TIME PETRI NETS [J].
BERTHOMIEU, B ;
DIAZ, M .
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1991, 17 (03) :259-273
[3]   A CALCULUS OF DURATIONS [J].
CHAOCHEN, Z ;
HOARE, CAR ;
RAVN, AP .
INFORMATION PROCESSING LETTERS, 1991, 40 (05) :269-276
[4]  
KESTEN Y, 1993, LECTURE NOTES COMPUT, V736, P179
[5]  
LILIUS J, 1998, P MFCS WORKSH CONC B, V18
[6]   RECOVERABILITY OF COMMUNICATION PROTOCOLS - IMPLICATIONS OF A THEORETICAL-STUDY [J].
MERLIN, PM ;
FARBER, DJ .
IEEE TRANSACTIONS ON COMMUNICATIONS, 1976, 24 (09) :1036-1043
[7]  
XUANDONG L, 1997, LECT NOTES COMPUT SC, V1345, P166
[8]   Efficient verification of parallel real-time systems [J].
Yoneda, T ;
Schlingloff, BH .
FORMAL METHODS IN SYSTEM DESIGN, 1997, 11 (02) :187-215
[9]  
ZHOU C, 1994, LECT NOTES COMPUT SC, V863, P88
1