Slicing Communicating Automata Specifications for Efficient Model Reduction

Slicing is a program analysis technique, originally aimed at helping software engineers in program debugging. A slicing algorithm is intended to remove unnecessary statements, with respect to a criterion. Nowadays, slicing is becoming more important on the specification level, for model reduction. Our contribution consists of a dependence-based solution to the problem of slicing communicating automata specifications, together with efficient algorithms to automatically extract slices. The resulting slicing tool - named CARVER - has shown to be operational in specification debugging and understanding. The model reduction results obtained with this tool are promising, notably in the area of formal validation and verification.