Design Validation of ZCSP with SPIN

— 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 nonfinite 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.

• Type: Conference
• Year: 2003
• Where: ACSD
• Authors: Vincent Beaudenon, Emmanuelle Encrenaz, Jean Lou Desbarbieux
• Keywords: ACSD 2003, Copy Secured Protocol, Hardware, SPIN Model Checker, first Model