Fases Para Implementar Model Checking

Para implementar Model checking se siguen tres fases:

Fase de modelado: En esta fase se modela el sistema utilizando un lenguaje de descripción de modelos.

Los modelos de sistemas describen elcomportamiento de sistema utilizando autómatas de estado finito, es decir, consisten en un conjunto finito de estados y en un conjunto finito de transiciones. Los estados se refieren a los valoresactuales de las variables, las sentencias previas ejecutadas. Las transiciones describen la transformación del sistema de un estado a otro.

Para hacer una validación rigurosa, las propiedades debenestar descritas utilizando un lenguaje de especificación de propiedades basado en la lógica temporal, que permite la especificación de propiedades relevantes para los sistemas concurrentes.

Entérminos de lógica matemática, se valida que la descripción del sistema es un modelo de una fórmula de lógica temporal. Esto explica el término de model cheking. La lógica temporal es básicamente unaextensión de una lógica proposicional 0con operadores que hacen referencia al comportamiento de los sistemas en el tiempo.

Lo descrito anteriormente nos muestra como la técnica de model cheking permitemediante la lógica temporal validar las propiedades de un sistema como las que se describen a continuación:

Corrección funcional, es decir, si el sistema hace lo que debe hacer.

Accesibilidad paradeterminar si es posible que el sistema termine en un estado de bloqueo (deadlock).

Seguridad de que nunca va a ocurrir ningún error en el sistema.

Viveza para determinar si algo bueno ocurrir‘a eventualmente en el sistema.

Justicia, es decir, determinar si ciertas condiciones ocurren repetidamente en el sistema.

Tiempo real para determinar si los eventos del sistema se están ejecutandoa tiempo.

A pesar de que lo descrito anteriormente para modelar un sistema se comprende a la perfección, es difícil determinar si un sistema es una adecuada descripción para la verificación...