Slicing communicating automata specifications: polynomial algorithms for model reduction

Abstract. Slicing is a program analysis technique that was originally introduced to improve program debugging and understanding. The purpose of a slicing algorithm is to remove the statements whose execution is not necessary with respect to some point(s) of interest in the program (called slicing criterion). Nowadays, slicing is becoming more important on the specification level, in particular for model reduction. In this article we propose a dependence-based solution to the problem of slicing communicating automata formal specifications. Dependence relations in specifications are formally defined. Efficient algorithms are provided to compute the dependence relations, and use this information to automatically extract slices. All the algorithms have been implemented in a slicing prototype tool, that has shown to be operational in specification debugging and understanding. The model reduction results obtained with our slicer are promising, notably in the area of formal validation and ver...

• Type: Journal
• Year: 2008
• Where: FAC
• Authors: Sébastien Labbé, Jean-Pierre Gallois
• Keywords: Dependence Relations, FAC 2008, Model Reduction, Specification