Logo Nabla Nantes B Libraries Page  
(Etude de cas : Controle d'accès)
sdssssssscbvcbvsssslhkhhkjhkjhkjhkhkjkjhkssssssdsdsdsdsdsdsdsdsdssd
Nantes B Libraries (Libraries of B specifications and development approaches)  
 Keywords : B specifications, Reuse, Libraries, Reuse Techniques Presentation 
 
Projet / Project :  Systèmes de controle d'accès Participants : 
Duc, Renaud, LeGallo,
Elek, Chahwekilian
 status : en cours
Description :
Il s'agit de concevoir et développer un système (logiciel) pour contr\^oler l'accès à un ensemble de batiments. Ce cahier de charges est initialement proposé dans le cadre d'une conférence AFADL).

Un b\^atiment dispose de plusieurs portes d'accès en entrée et en sortie.
Chaque porte d'entrée ou de sortie dispose d'un lecteur de carte. Un voyant rouge et un voyant vert sont associés à chaque lecteur.
Chaque carte est identifiée par un numéro unique.
Une carte peut \^etre volée ou perdue.

Les usagers des batiments ont chacun une carte (d'accès).
Les usagers des batiments sont organisés en groupe et les groupes ont accès ou non à certains batiments.

Il y a un protocole pour entrer et sortir d'un batiment. \\
Pour entrer dans un batiment, un usager se présente devant une porte d'entrée, il passe sa carte dans le lecteur. Si l'usager est autorisé à entrer dans le batiment, le voyant vert du lecteur s'allume. La porte est débloquée, l'usager a alors 30s pour passer la porte. Après 30 s la porte est bloquée si l'usager n'est pas passé. Le voyant vert s'allume de nouveau.
Si l'usager n'est pas autorisé à entrer dans la batiment, le voyant rouge s'allume pendant 2s, la porte reste bloquée, le voyant vert étant eteint.

Pour sortir d'un b\^atiment l'usager se présente à une porte de sortie et passe sa carte dans le lecteur associée à cette porte. Il sort du batiment quand les vérifications necessaires sont faites.

Un journal des entrées/sorties des batiments est tenu à jour. On y note les entrées  et les sorties (carte, heure, porte). On peut donc savoir a tout moment les usagers qui se trouvent dans les batiments.

Les batiment peuvent communiquer les uns avec les autres.
 
Le système de controle des accès doit garantir quelques propriétés de bon fonctionnement, par exemple, aucun usager ne peut \^etre dans plus d'un batiment à la fois. Si un usager est dans un batiment, il y est autorisé et il est passé par une des portes d'entrée de ce batiment, etc.
 

Dans une première étape du travail, on fait quelques hypothèses : les usagers sont disciplinés, ils utilisent le protocole d'accès correctement (pas de fraude).
 


Contact : email  
LINA/COLOSS  
Méthodes et Spécifications Formelles 
Addresse  
IRIN - Faculté des sciences  
 2, rue de la Houssinière BP 92298  
44 322 Nantes Cedex 3