Symmetric nets get better tools for checking system properties
Semi-automated Verification of Symbolic Invariants In Extended Symmetric Nets
Symbolic ComputationSoftware Engineering
Summary
Systems called Symmetric Nets help model complex behaviors with repeated or similar parts, but checking their properties is hard and often slow. The authors improved a method to semi-automatically verify certain properties called invariants in a more general type of Symmetric Nets, called Extended Symmetric Nets. They use advanced symbolic techniques that avoid exploring every possible system state. Their work helps verify these systems more efficiently and could lead to more reliable designs in complex fields.
What this means in practice
- •For software verification engineers: Check consistency and safety properties of complex concurrent software systems modeled with extended symmetric nets more efficiently.
- •For systems modelers in manufacturing: Model and verify resource conflicts and process flows symbolically in automated production systems using extended symmetric nets.
Tested on simulated data.
Authors
Lorenzo Capra
Abstract
Structural analysis is central to Petri Net (PN) research, complementing state-space methods while avoiding their combinatorial issues. It is well studied for classical PNs but much less for High-Level Petri Nets (HLPN). Symmetric Nets (SN), a common HLPN formalism, use compact annotations to encode behavioral symmetries, allowing symbolic reachability graphs and associated lumped Markov chains for stochastic SN. In the past two decades, specific structural techniques for SN have emerged, notably the SNexpression tool, which implements a calculus for symbolic structural relations such as conflict and causality. We propose using this calculus to semi-automatically verify symbolic structural invariants, currently possible only for restricted SN subclasses, for an extended SN formalism (ESN) closed under key functional operators. We focus on flows and outline, at least in theory, how to construct a flow-generating family. We also sketch a framework for formally verifying a wider range of invariant properties. Representative examples illustrate the main concepts.