Mechanical Abstraction of CSPZ Processes

We propose a mechanised strategy to turn an infinite CSPZ process (formed of CSP and Z constructs) into one suitable for model checking. This strategy integrates two theories which allow us to consider the infiniteness of CSPZ as two separate problems: data independence for handling the behavioural aspect and abstract interpretation for handling the data structure aspect. A distinguishing feature of our approach to abstract interpretation is the generation of the abstract domains based on a symbolic execution of the process.