Enhancing the Formal Verification of Train Control Systems based on Decomposition.

Great achievements have improved the efficiency and effectiveness of formal verification fairly, such that it is now applicable to industrial-scale software. However, verifying a full software system is still considered too complex. In practice, industrial control software models to be verified may result in state space explosion. We propose a problem frame-based approach that takes the full software system as input and tries to decompose the full software model into some smaller modules. Our approach decomposes the whole safety requirements to sub safety requirements, and the verification problem of the whole model is projected to sub verification problem according to the decomposed safety requirements. The sub verification problems check the projected sub models against the the sub safety requirements. We carry out an extensive evaluation based on the trackside subsystems in rail transit. Verifying the decomposed model can lead to a significant performance gain, due to the fact that abstract models reduce too much state space.