Modélisation d’un système de contrôle automatique des trai

Notions spécifiques au cas d’étude Synchronisation quantifiée conditionnelle

L’opérateur de synchronisation quantifiée conditionnelle (symbole t) est une extension de l’opérateur de synchronisation quantifiée. Soit ht, n, x, T, ∆, p, bi l’ensemble des astd de type synchronisation quantifiée conditionnelle, où n est le nom de l’astd, x une variable choisie dans l’ensemble T, ∆ est l’ensemble des étiquettes de transition qui sont synchronisées, p est un prédicat et b est un astd. Cet opérateur signifie que l’astd b est exécuté en autant d’instances x qu’il y a de valeurs dans l’ensemble T. Ces instances sont exécutées en entrelacement, mais doivent se synchroniser pour toutes les transitions dont l’étiquette se trouve dans l’ensemble ∆, sauf pour les instances pour lesquelles le prédicat p n’est pas vrai. Plus formellement, les règles d’inférences pour exécuter une transition dans un astd en synchronisation quantifiée conditionnelle sont les suivantes

La règle t1 décrit la possibilité d’exécuter une transition n’appartenant pas à l’ensemble de synchronisation

La règle t2 décrit la possibilité d’exécuter une transition appartenant à l’ensemble de synchronisation ∆. Elle signifie qu’il est possible d’exécuter une telle transition si pour toutes les instances de l’ensemble de quantification T, soit le prédicat p est faux pour cette instance et l’état associé à l’instance ne change pas ([x := v]p ∧ f(v) = f 0 (v)), soit l’instance est dans un état permettant la transition, et la transition est alors exécutée (f(v) σ,([x:=v])2Γ −−−−−−−→ f 0 (v)).

Cet opérateur permet de décrire le comportement de plusieurs instances fonctionnant en parallèle tout en évitant de créer des situations dans lesquelles des instances sont bloquées par d’autres pour exécuter une transition synchronisée. Dans la spécification de ce cas d’étude par exemple, nous modélisons un ensemble de trains qui peuvent être démarrés et arrêtés.

Nous souhaitons alors que les trains arrêtés ne puissent pas bloquer les autres trains qui doivent exécuter une transition synchronisée. Pour un exemple plus précis, voir le troisième raffinement dans la section 5.1.3. On remarquera que la synchronisation quantifiée des astd (dont les règles d’inférence sont données en Annexe A.7) est le cas particulier de la synchronisation quantifiée conditionnelle où le prédicat p de condition de synchronisation est le prédicat true, qui est toujours vrai. 

Transformation d’un entrelacement en synchronisation

Dans le système que nous souhaitons modéliser, nous voulons transformer un système dans lequel plusieurs instances s’exécutent en parallèle en un système dans lequel les différentes instances sont synchronisées sur une transition. Soit un astd abstrait A = ht, n, x, T, ∆, p, bi de type synchronisation quantifiée conditionnelle et soit une étiquette de transition non synchronisée σ(x) (σ(x) ∈/ ∆) qui prend x en paramètre.

Nous souhaitons transformer l’astd A en l’astd C = ht, n, T, ∆∪σ, p, b0 i où σ remplace toutes les transitions σ(x) qui doivent être exécutées en même temps en se synchronisant. L’astd b 0 est donc l’astd b dans lequel toutes les transitions ayant pour étiquette σ(x) ont été remplacées par une transition étiquetée σ. Cette transformation ne vérifie pas la définition du raffinement des astd donnée à la section 2.3. En effet, dans la spécification abstraite, pour une instance v, il est possible d’exécuter la transition σ si l’instance v est dans un état qui permet d’exécuter σ.

Dans la spécification concrète, il faut attendre pour exécuter σ que toutes les instances qui doivent se synchroniser soient dans un état qui leur permet d’exécuter σ. Un certain nombre de traces ne sont donc pas préservées dans la spécification concrète. Cependant, dans le cas où cette transformation est utilisée dans le cas d’étude présenté ci-après, pour toute instance devant se synchroniser (toute instance vérifiant le prédicat p), la spécification permet d’exécuter un cycle de transitions (une séquence de transition qui revient au même état) au cours duquel les variables d’état ne sont pas modifiées, et ce cycle contient la transition σ synchronisée.

Dans ce cas, il est possible d’ajouter à toute trace un tel cycle de transitions sans véritablement changer le comportement observé. Si cette condition est vraie pour un système, il est possible de trouver une trace équivalente à toutes les traces abstraites dans les traces concrètes. On dit ici que deux traces sont équivalentes si quelque soit l’état des données avant l’exécution de chaque trace, les données sont dans le même état après l’exécution des deux traces.