Hippo-CPS: A Tool for Verification and Analysis of Petri Net-Based Cyber-Physical Systems

被引：3

作者：

Wisniewski, Remigiusz ^{[1
]}

Bazydlo, Grzegorz ^{[1
]}

Wojnakowski, Marcin ^{[1
]}

Poplawski, Mateusz ^{[1
]}

机构：

[1] Univ Zielona Gora, Inst Control & Computat Engn, Ul Prof Z Szafrana 2, PL-65516 Zielona Gora, Poland

来源：

APPLICATION AND THEORY OF PETRI NETS AND CONCURRENCY, PETRI NETS 2023 | 2023年 / 13929卷

关键词：

Verification; Analysis; Petri net; Cyber-physical system; Boundedness; Safety; Liveness; Invariants; Reachability tree; CONCURRENT CONTROL-SYSTEMS; DYNAMIC PARTIAL RECONFIGURATION; DEADLOCK PREVENTION POLICY;

D O I：

10.1007/978-3-031-33620-1_10

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

The paper deals with the verification and analysis techniques offered by the Hippo-CPS system. The presented tool offers alternate examination methods of the Petri net-based cyber-physical system. In particular, the set of proposed modules permits the classification of the system, verification of its main properties (such as liveness, boundedness, and safeness), and the performance of advanced concurrency and sequentiality analysis of the system (including state-space analysis, place invariant analysis, state machine component-based analysis, etc.). Although the paper is focused on the Hippo-CPS application, the presented tools have a strong theoretical background, including adequate algorithms, theorems, and proofs. The functionality of the tools was verified experimentally, by examination of the efficiency and effectiveness of the implemented techniques.

引用

页码：191 / 204

页数：14