Hybrid trace nets speed up safety checks in complex systems
Structural Analysis of Hybrid-Trace Nets: An Optimization Approach
Logic in Computer Science
Summary
Checking if complex safety-critical systems can reach dangerous states is very hard because there are so many possible situations to consider. The authors offer a new way to relax this problem using hybrid trace nets, which makes it faster and easier to find important conditions that always hold in safe situations. Their method can prove unsafe states don’t happen more often and find these helpful conditions much faster than older approaches. This helps simplify the system’s analysis and lets verification run more efficiently.
What this means in practice
- •For safety engineers: Verify safety properties of complex concurrent systems with faster state-space exploration by using hybrid trace net relaxations to find invariants and prove unsafe states unreachable.
- •For embedded systems developers: Enhance fault detection in embedded software by integrating invariant-based relaxations from hybrid trace nets to reduce verification time and improve efficiency.
Authors
Nguyen Cong Nhat Le, Claire N. Bonial, John G. Rogers, Neil T. Dantam
Abstract
Fault and error detection is crucial for ensuring the correctness of safety-critical systems. Safety verification often addresses reachability of bad system states, where exhaustive state inspection may be intractable due to the large state spaces of complex systems. We propose a reachability relaxation for hybrid trace nets, a useful mathematical model for analyzing concurrent event systems, to efficiently verify system safety. We further use our relaxation to effectively identify invariants, expressions that hold in all reachable states, allowing state-space reduction for efficient verification. Empirically, our approach proves unsafe states unreachable in 1.5x more instances, generates 2.5x more invariants with up to 2 orders of magnitude faster generation times than the baselines in the tested problems.