Bounded Model Checking of PLC ST Programs using Rewriting Modulo SMT
summary
Extends ST semantics to model scan cycles, program scheduling and timers so PLC behavior is cyclic and time-aware, then reduces LTL model checking to existential reachability and solves it symbolically with rewriting modulo SMT. Implements the method in tool sdbmc, verifies a traffic-light case study where it finds a concrete input sequence counterexample for a green→red rule, the bug is fixed and rechecked. Benchmarks on 14 models (32–2,000+ lines) show comparable performance to PLCverif/CBMC without extra optimizations.
AI-written summary · about
chapters (14)
- 0:00PLC and model checking intro
- 1:31Existing PLC verification
- 3:38K framework semantics
- 5:46Limitations of prior work
- 7:09Our contribution overview
- 10:49PLC scan cycle scheduling
- 12:32Time features in PLC
- 15:05Rewriting modulo SMT
- 16:52Bounded LTL model checking
- 17:55Traffic light case study
- 20:44Debugging counterexamples
- 21:30Experimental results
- 22:39Comparison with tools
- 23:24Q&A
related talks
20mPlankton: Scalable network configuration verification through model checking
16mSoftware Model Checking via Summary-Guided Search
24mTLA+: Your Secret Weapon Against Concurrency Hell
34mAbstract Interpretation, Software Model Checking, and Beyond - A Celebration of the(…)
21mBounded-Exhaustive Subspace Diversification for SMT Solver Testing
24mBuilding Information Modeling Using Constraint Logic Programming (Extended Ab...
31mGenerating Constraint Programs for Variability Model Reasoning: A DSL and Solver-...
01h 09mPlenary: Neighborhoods Banding Together: Reasoning Globally about Programs