Rapport de Recherche LIP6 /
8 pages - Janvier/January 2003 - Document en anglais.
Get it : 190 Ko /Kb
Contact : par mail / e-mail
Thème/Team: Architecture des Systèmes Intégrés et Micro-Électronique
Titre français : Validation Formelle du protocole ZCSP avec SPIN
Titre anglais : Design Validation of ZCSP with SPIN
Abstract : We consider the problem of specifying a model of a Zero Copy Secured Protocol for LTL verification purpose with the Model Checker SPIN. ZCSP is based on Direct Memory Access. Datas are 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. Two main steps were performed : A finite and a none finite sequences model. The first model gave us an overview of the protocol robustness. The second allowed us to test realistics properties. We also describe LTL properties that were checked with the SPIN model checker. Unfortunately the size of the system is frequently prohibitive. Thus, we explain all minimization we had to perform.
Key-words : Model Checking, SPIN, ProMeLa, ZCSP, LTL
Publications internes LIP6 2002 / LIP6 research reports 2002
Responsable Éditorial / Editor :Francois.Dromard@lip6.fr