Sciweavers

Share
ACSD
2003
IEEE

Design Validation of ZCSP with SPIN

10 years 3 months ago
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.
Vincent Beaudenon, Emmanuelle Encrenaz, Jean Lou D
Added 04 Jul 2010
Updated 04 Jul 2010
Type Conference
Year 2003
Where ACSD
Authors Vincent Beaudenon, Emmanuelle Encrenaz, Jean Lou Desbarbieux
Comments (0)
books