Symmetry reduction for time Petri net state classes

被引：14

作者：

Bourdil, Pierre-Alain ^{[1
,3
]}

Berthomieu, Bernard ^{[1
]}

Dal Zilio, Silvano ^{[1
]}

Vernadat, Francois ^{[1
,2
]}

机构：

[1] Univ Toulouse, CNRS, LAAS, Toulouse, France

[2] Univ Toulouse, CNRS, LAAS, INSA, Toulouse, France

[3] Eurogiciel Ingn, 417 Ave Occitane, F-31670 Labege, France

来源：

SCIENCE OF COMPUTER PROGRAMMING | 2016年 / 132卷

关键词：

Time Petri nets; State classes; Symmetry reduction; SYSTEMS; VERIFICATION; SAFETY;

D O I：

10.1016/j.scico.2016.08.008

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We propose a method to exploit the symmetries of a real-time system represented by a Time Petri net for its verification by model-checking. The method handles both markings and timing constraints; it can be used in conjunction with the widely used state classes abstraction, a construction providing a finite representation of the behavior of a Time Petri net preserving its markings and traces. The approach has been implemented and experiments are reported. (C) 2016 Elsevier B.V. All rights reserved.

引用

页码：209 / 225

页数：17

共 35 条

[1]

Bérard B, 2005, LECT NOTES COMPUT SC, V3829, P211

[2]

Berthomieu B., 1983, Information Processing 83. Proceedings of the IFIP 9th World Computer Congress, P41

[3]

Berthomieu B, 2004, INT J PROD RES, V42, P2741, DOI 10.1080/00207540410001705257

[4]

Berthomieu B, 2003, LECT NOTES COMPUT SC, V2619, P442

[5] 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

[6]

BERTHOMIEU B, 2007, HDB REAL TIME EMBEDD

[7]

Berthomieu B, 2006, LECT NOTES COMPUT SC, V4202, P82

[8]

Boucheneb H., 2003, Technique et Science Informatiques, V22, P435, DOI 10.3166/tsi.22.435-459

[9]

Bourdil P.-A., 2015, THESIS

[10] Oris: A tool for modeling, verification and evaluation of real-time systems [J].

Bucci G. ;

Carnevali L. ;

Ridi L. ;

Vicario E. .

International Journal on Software Tools for Technology Transfer, 2010, 12 (5) :391-403

← 1 2 3 4 →