| 摘要 |
Procedimiento de verificación de un sistema modelizado por un sistema (S) de autómatas sincronizados por un conjunto de mensajes (M), que comprende las operaciones siguientes: se descompone el sistema en un número N de subsistemas numerados de n=1 a n=N; se facilitan parámetros que describen cada uno de los subsistemas n, 1 n N, en forma de un autómata respectivo (Sn) compuesto de un conjunto En de estados e i n del subsistema n, con un conjunto An de transiciones a j n entre pares de estados del conjunto En, estando asociada cada transición a j n del conjunto An a un subconjunto M j n del conjunto de mensajes de sincronización (M), de manera que se traduce el hecho que cada mensaje del subconjunto M j n tiene lugar cuando el subsistema describe cambio de estado de acuerdo con la transición a j n ; se construye un sistema de ecuaciones lineales (1f, 2f, 3s) que comprende, para 1 t T y 1n N, por una parte ecuaciones flotantes de forma: e i n (t 1) = X j2B i n a j n (t) para e i n 2 En y delaforma: e i n (t) = X j2C i n a j n (t) para e i n 2 En; y por otra parte ecuaciones de sincronización de la forma: m k (t) = X j2D k n a j n (t) para m k 2 Mn; en las que T indica el número de etapas sucesivas de funcionamiento del sistema, B i n designa el conjunto de los índices j tales que la transición a j n del conjunto An procede del estado e i n del conjunto En, C i n indica el conjunto de los índices j tales que la transición a j n del conjunto An conduce al estado e i n del conjunto En, Mn designa la reunión de los subconjuntos de mensajes M j n respectivamente asociados a las transiciones del conjunto An, D k n designa el conjunto de los índices j tales que un mensaje m k del conjunto Mn pertenece al subconjunto M j n asociado a la transición a j n del conjunto An, lavariablee i n (t)j 0 t T es una incógnita del sistema lineal asociado al estado e i n del conjunto En y a la etapa t, la variable a j n (t)(1 t T) es una incógnita del sistema lineal asociado a la transición a j n del conjunto An y en la etapa t, la variable m k (t), 1 t T, es una desconocida del sistema lineal asociado al mensaje m k del conjunto (M) de los mensajes de sincronización y en la etapa t; se dene una propiedad del sistema a verificar, en forma de condiciones lineales suplementarias impuestas a las incógnitas del sistema lineal; se aplica al sistema lineal sometido a las limitaciones suplementarias un método de resolución por programación lineal; y se analiza el resultado de la programación lineal para determinar si dicha propiedad es verificada por el sistema.
|
