We consider the problem of specifying a model of the Zero Copy Secured Protocol for the purpose of LTL verification with the SPIN Model Checker. ZCSP is based on Direct Memory Access. Data is directly read/written in user space memory, decreasing latency and saving processor computing time. We first introduce the ZCSP protocol before analysing different ways of modelling it.

Two main steps were performed: A finite and a non-finite sequences model. The first model gave us an overview of the protocol robustness. The second allowed us to test realistic properties. We also describe LTL properties that were checked with the SPIN model checker.

Unfortunately the size of the system was frequently prohibitive. Thus, we explain all minimization steps we had to perform: Variables? domains restriction, interleaving reduction, realistic environnement representation by fairness constraints.