Liveness and boundedness preservations of sharing synthesis of Petri net based representation for embedded systems

被引：2

作者：

Xia, Chuanliang ^{[1
]}

Shen, Bin ^{[1
]}

Zhang, Hailin ^{[1
]}

Wang, Yigui ^{[1
]}

机构：

[1] Shandong Jianzhu Univ, Sch Comp Sci & Technol, Jinan 250101, Shandong, Peoples R China

来源：

COMPUTER SYSTEMS SCIENCE AND ENGINEERING | 2018年 / 33卷 / 05期

基金：

中国国家自然科学基金;

关键词：

Petri nets; synthesis; liveness; property preservation; modeling; FORMAL VERIFICATION; MODELS;

D O I：

暂无

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

Petri net based Representation for Embedded Systems (PRES+) is an outstanding methodology for analysis, modeling and verification of embedded systems. State space explosion is an awful problem for PRES+ to model and analyze large complex embedded systems. In order to solve this problem, we concern with a method for expending PRES+ model by using synthesis approach. A kind of sharing synthesis operation for PRES+ is proposed in this paper. Under some conditions liveness and boundedness will be preserved by using this sharing synthesis approach. An applicable example in the form of an embedded control system illustrates the useful of our synthesis method. These results can be nicely used to investigate dynamic properties of large embedded systems.

引用

页码：345 / 350

页数：6

共 22 条

[1]

Bandyopadhyay Soumyadip, 2012, Progress in VLSI Design and Test. Proceedings 16th International Symposium, VDAT 2012, P69, DOI 10.1007/978-3-642-31494-0_9

[2] A branch and bound approach for the design of decentralized supervisors in Petri net models [J].

Basile, Francesco ;

Cordone, Roberto ;

Piroddi, Luigi .

AUTOMATICA, 2015, 52 :322-333

[3] Automated synthesis of hybrid Petri net models for robotic cells in the aircraft industry [J].

Basile, Francesco ;

Caccavale, Fabrizio ;

Chiacchio, Pasquale ;

Coppola, Jolanda ;

Marino, Alessandro ;

Gerbasio, Diego .

CONTROL ENGINEERING PRACTICE, 2014, 31 :35-49

[4] Characterisation of the state spaces of marked graph Petri nets [J].

Best, Eike ;

Devillers, Raymond .

INFORMATION AND COMPUTATION, 2017, 253 :399-410

[5] Modeling and formal verification of embedded systems based on a Petri net representation [J].

Cortés, LA ;

Eles, P ;

Peng, Z .

JOURNAL OF SYSTEMS ARCHITECTURE, 2003, 49 (12-15) :571-598

[6] Hierarchical modeling and verification of embedded systems [J].

Cortés, LA ;

Eles, P ;

Peng, Z .

EUROMICRO SYMPOSIUM ON DIGITAL SYSTEMS DESIGN, PROCEEDINGS, 2001, :63-70

[7]

Cortés LA, 2000, IEEE INT C ENG COMP, P134, DOI 10.1109/ICECCS.2000.873937

[8] Petri games: Synthesis of distributed systems with causal memory [J].

Finkbeiner, Bernd ;

Olderog, Ernst-Ruediger .

INFORMATION AND COMPUTATION, 2017, 253 :181-203

[9] Polynomially Complex Synthesis of Distributed Supervisors for Large-Scale AMSs Using Petri Nets [J].

Hu, Hesuan ;

Su, Rong ;

Zhou, MengChu ;

Liu, Yang .

IEEE TRANSACTIONS ON CONTROL SYSTEMS TECHNOLOGY, 2016, 24 (05) :1610-1622

[10] Service net algebra based on logic Petri nets [J].

Hu, Qiang ;

Du, Yuyue ;

Yu, ShuXia .

INFORMATION SCIENCES, 2014, 268 :271-289

← 1 2 3 →