Decomposing Integrated Specifications for Verification

摘要

Integrated formal specifications are intrinsically difficult to (automatically) verify due to the combination of complex data and behaviour. In this paper, we present a method for decomposing specifications into several smaller parts which can be independently verified. Verification results can then be combined to make a global result according to the original specification. Instead of relying on an a priori given structure of the system such as a parallel composition of components, we compute the decomposition by ourselves using the technique of slicing. With less effort, significant properties can be verified for the resulting specification parts and be applied to the full specification. We prove correctness of our method and exemplify it according to a specification from the rail domain.