MODELING AND VERIFICATION OF TIME-DEPENDENT SYSTEMS USING TIME PETRI NETS

被引：533

作者：

BERTHOMIEU, B ^{[1
]}

DIAZ, M ^{[1
]}

机构：

[1] CNRS,AUTOMAT ANAL SYST RES GRP,SOFTWARE & TOOLS COMMUN SYST,F-31077 TOULOUSE,FRANCE

来源：

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING | 1991年 / 17卷 / 03期

关键词：

MODELING; PARALLEL AND DISTRIBUTED SYSTEMS; SPECIFICATION; TIME; TIME PETRI NETS; VERIFICATION;

D O I：

10.1109/32.75415

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

This paper deals with describing and analyzing concurrent systems, such as communication systems, whose behavior is dependent on explicit values of time. An enumerative method is proposed in order to exhaustively validate the behavior of Merlin's time Petri net models. This new method, which allows one to formally verify time dependent systems, is applied to a simple illustrative example, the specification and verification of the alternating bit protocol.

引用

页码：259 / 273

页数：15

共 30 条

[1]

[Anonymous], 2003, LINEAR PROGRAMMING

[2]

Aspvall B., 1979, 20th Annual Symposium of Foundations of Computer Science, P205, DOI 10.1109/SFCS.1979.1

[3]

AYACHE JM, 1982, IEEE T COMPUT, V31

[4]

BARTLETT KA, 1969, COMMUN ACM, V12

[5]

BERTHOMIEU B, 1982, 3RD P EUR WORKSH APP

[6]

BERTHOMIEU B, 1983, SEP P IFIP C PAR

[7]

CASPI P, 1981, 2ND P WORKSH APPL TH

[8]

CASPI P, 1982, RR322 LAB INF MATH A

[9]

CHRETIENNE P, 1981, 2ND P WORKSH APPL TH

[10]

DANTHINE AS, 1980, IEEE T COMMUN, V28

← 1 2 3 →