A toolchain on model checking SPIN via Kalman Decomposition for control system software
Tsukada Kento, Kenji Sawada, Seiichi Shin · 2016
This paper proposes a new model checking method to detect falsification on control system software. In the previous study, we have examined a method which detects illegal rewriting for control system software via Petri Net and Kalman Decomposition (KD). In this paper, in order to divert this method to model checking, we consider a new toolchain with the existing model checker SPIN. Specifically, we develop a tool that translates Petri Net into Promela (modeling language of SPIN) and clarify that KD allows us to generate Linear Temporal Logic (LTL) formulas for SPIN automatically. In addition, we give a simple example of applying SPIN to Petri Net models before and after falsification.