Scribd
Importer
18 vues2 pages

Modélisation du contrôle d'ascenseur

Le document présente un TD sur la modélisation des systèmes réactifs, en utilisant l'exemple d'un ascenseur pour illustrer le contrôle et les états du système. Il aborde également des exercices sur la concurrence et la sûreté, en posant des questions sur les transitions des systèmes concurrents et les propriétés de sûreté des opérations de verrouillage. Enfin, il demande de définir des automates pour vérifier certaines propriétés liées aux opérations de verrou.

Transféré par

cbennouri70
Copyright
© All Rights Reserved
Nous prenons très au sérieux les droits relatifs au contenu. Si vous pensez qu’il s’agit de votre contenu, signalez une atteinte au droit d’auteur ici.
Formats disponibles
Téléchargez aux formats PDF, TXT ou lisez en ligne sur Scribd
18 vues2 pages

Modélisation du contrôle d'ascenseur

Le document présente un TD sur la modélisation des systèmes réactifs, en utilisant l'exemple d'un ascenseur pour illustrer le contrôle et les états du système. Il aborde également des exercices sur la concurrence et la sûreté, en posant des questions sur les transitions des systèmes concurrents et les propriétés de sûreté des opérations de verrouillage. Enfin, il demande de définir des automates pour vérifier certaines propriétés liées aux opérations de verrou.

Transféré par

cbennouri70
Copyright
© All Rights Reserved
Nous prenons très au sérieux les droits relatifs au contenu. Si vous pensez qu’il s’agit de votre contenu, signalez une atteinte au droit d’auteur ici.
Formats disponibles
Téléchargez aux formats PDF, TXT ou lisez en ligne sur Scribd

TD 1 de ModelChecking

Modélisation des systèmes réactifs


Exercice 1 (Exemple de l’ascenceur.). Le système de contrôle d’un ascenceur (pour 3 étages) est défini par :
– le contrôleur garde en mémoire l’étage courant et l’étage cible.
– en mode actif, quand l’étage cible est atteint, les portes s’ouvrent et le contrôleur passe en mode attente.
– en mode actif, quand l’étage cible est plus élevé que l’étage courant, le contrôleur fait s’élever l’as-
cenceur.
– en mode actif, quand l’étage cible est moins élevé que l’étage courant, le contrôleur fait descendre
l’ascenceur.
– en mode attente, il se peut que quelqu’un entre dans l’ascenceur et choisisse un nouvel étage cible.
L’ascenceur ferme alors les portes et redevient actif.
– initialement, l’ascenceur est à l’étage 0 et en mode attente.
Questions : 1. Proposez une machine à états modélisant le contrôle de l’ascenceur (définition formelle et
dessin). 2. Définissez et dessinez le système de transitions correspondant (en vous limitant aux configurations
accessibles depuis l’état initial). 3. Est-ce que les portes peuvent s’ouvrir quand l’ascenceur est actif ?
Exercice 2 (Concurrence). Soit les machines concurrentes suivantes.
1 3
5

2 4

Quelles sont les transitions du système concurrent dans les cas suivants :
1. sémantique synchrone + synchronisation entre 1 et 3 ;
2. sémantique asynchrone + synchronisation entre 1 et 3 ;
Quel est le lien entre vecteur de synchronisations et rendez-vous ?
Exercice 3 (Sûreté). On se donne un système de transitions S dont certaines transitions sont distinguées
et correspondent à des opérations d’aquisition de verrou (lock), de rendu de verrou (unlock), de lecture
(read) et d’écriture (write). On se donne la propriété ϕ suivante :
Si on ne regarde que les lock et unlock : unlock est toujours précédé directement de lock, ET une
suite arbitraire de read,write est toujours précédée directement d’un lock .
Questions :
1. Est-ce que ϕ est une propriété de sûreté ? Sinon modifiez là en conséquence.
2. Écrivez un automate observeur pour vérifer ϕ (ou sa modification) et expliquez la nouvelle propriété à
vérifier.

1
3. On considère maintenant la spécification :
Si on ne regarde que les lock et unlock : unlock est toujours précédé directement de lock, ET une
suite arbitraire de read,write est toujours précédée directement d’un lock et fermée directement par
un unlock.
Est-ce toujours une propriété de sûreté ?

Vous aimerez peut-être aussi