SP-DEVS
SP-DEVS, que abrevia "Especificación del sistema de eventos discretos de conservación de la programación", es un formalismo para modelar y analizar sistemas de eventos discretos tanto en forma de simulación como de verificación. SP-DEVS también proporciona funciones de modelado modular y jerárquico que han sido heredadas de Classic DEVS .
SP-DEVS ha sido diseñado para respaldar el análisis de verificación de sus redes al garantizar la obtención de un gráfico de accesibilidad de vértice finito de las redes originales, que había sido un problema abierto del formalismo DEVS durante aproximadamente 30 años. Para obtener tal gráfico de accesibilidad de sus redes, SP-DEVS se ha impuesto las tres restricciones:
Por lo tanto, SP-DEVS es una subclase de DEVS y FD-DEVS . Estas tres restricciones hacen que la clase SP-DEVS se cierre bajo acoplamiento aunque el número de estados sea finito. Esta propiedad permite una verificación basada en gráficos de vértices finitos para algunas propiedades cualitativas y propiedades cuantitativas, incluso con modelos acoplados SP-DEVS.
Considere un sistema de cruce de peatones. Dado que una luz roja (resp. luz de no caminar) se comporta de manera opuesta a una luz verde (resp. luz de caminar), para simplificar, consideramos solo dos luces: una luz verde (G) y una luz de caminar (W ); y un botón como se muestra en la Fig. 1. Queremos controlar dos luces de G y W con un conjunto de restricciones de tiempo.
Para inicializar dos luces, se necesitan 0,5 segundos para encender G y 0,5 segundos más tarde, W se apaga. Luego, cada 30 segundos, existe la posibilidad de que G se apague y W se encienda si alguien presionó el botón. Por razones de seguridad, W se enciende dos segundos después de que G se apaga. 26 segundos después, W se baja y dos segundos después G vuelve a subir. Estos comportamientos se repiten.
Para construir un controlador para los requisitos anteriores, podemos considerar un evento de entrada 'pulsador' (abreviado como ?p) y cuatro eventos de salida 'encendido verde' (!g:1), 'apagado verde' (!g: 0), 'walk-on' (!w:1) y 'walk-off (!w:0) que se utilizarán como señales de comando para la luz verde y la luz para caminar. Como un conjunto de estados del controlador, consideramos 'booting-green' (BG), 'booting-walk' (BW), 'green-on' (G), 'green-to-red' (GR), ' rojo encendido' (R), 'walk-on' (W), 'retraso' (D). Diseñemos las transiciones de estado como se muestra en la Fig. 2. Inicialmente, el controlador comienza en BG, cuya vida útil es de 0,5 segundos. Después de la vida útil, se mueve al estado BW en este momento, también genera el evento 'green-on'. Después de permanecer 0,5 segundos en BW,pasa al estado G cuya vida útil es de 30 segundos. El controlador puede permanecer en G haciendo un bucle de G a G sin generar ningún evento de salida o puede pasar al estado GR cuando recibe el evento de entrada externo ?p. Pero elel tiempo real de permanencia en GR es el tiempo restante para el bucle en G. Desde GR, pasa al estado R generando un evento de salida !g:0 y su estado R dura dos segundos, luego pasará al estado W con el evento de salida !w :1. 26 segundos después, se mueve al estado D generando !w:0 y después de permanecer 2 segundos en D, regresa a G con el evento de salida !g:1.
