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

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.