The MEB and CEB static analysis for CSP specifications

Abstract. This work presents a static analysis technique based on pro-gram slicing for CSP specifications. Given a particular event in a CSP specification, our technique allows us to know what parts of the specifi-cation must necessarily be executed before this event, and what parts of the specification could be executed before it in some execution. Our tech-nique is based on a new data structure which extends the Synchronized Control Flow Graph (SCFG). We show that this new data structure im-proves the SCFG by taking into account the context in which processes are called and, thus, makes the slicing process more precise