stringtranslate.com

Comprobador de modelos TAPA

TAPAs es una herramienta para especificar y analizar sistemas concurrentes. Su objetivo es apoyar la enseñanza de álgebras de procesos. Los sistemas se describen como términos de álgebra de procesos que luego se asignan a sistemas de transición etiquetados (LTS). Las propiedades se pueden verificar comprobando las equivalencias entre descripciones de sistemas concretos y abstractos o comprobando fórmulas temporales de modelos (expresadas como μ-cálculo o ACTL ) sobre el LTS obtenido. Una característica clave de TAPAs que lo hace particularmente adecuado para la enseñanza es que mantiene una representación gráfica y textual consistente de cada sistema. Después de un cambio en la notación gráfica, la representación textual se actualiza inmediatamente; pero después de las modificaciones textuales, la actualización de la representación gráfica debe activarse manualmente.

En TAPAs, los sistemas concurrentes se describen por medio de procesos, que son descripciones no deterministas de comportamientos de sistemas, y sistemas de procesos, que se obtienen mediante composiciones de procesos. En particular, los procesos se pueden definir en términos de otros procesos o sistemas de procesos. Los procesos y los sistemas de procesos se componen mediante el uso de los operadores de un álgebra de procesos determinada. Actualmente, TAPAs admite dos álgebras de procesos: CCSP y PEPA .

El CCSP (= CCS + CSP ) se obtiene a partir del CCS considerando algunos operadores de CSP . Después de crear un sistema de proceso CCSP, el usuario puede analizarlo utilizando una de las siguientes herramientas.

PEPA (Performance Evaluation Process Algebra) es un álgebra de procesos estocásticos diseñada para modelar sistemas informáticos y de comunicación, introducida por Jane Hillston en la década de 1990. El lenguaje extiende las álgebras de procesos clásicas, como CCS de Milner y CSP de Hoare, al introducir ramificaciones probabilísticas y tiempos de transiciones. Las tasas se extraen de la distribución exponencial y los modelos PEPA son de estado finito, por lo que dan lugar a un proceso estocástico, específicamente un proceso de Markov de tiempo continuo ( CTMC ). Por lo tanto, el lenguaje se puede utilizar para estudiar propiedades cuantitativas de modelos de sistemas informáticos y de comunicación, como el rendimiento, la utilización y el tiempo de respuesta, así como propiedades cualitativas, como la ausencia de bloqueos. El lenguaje se define formalmente utilizando una semántica operacional estructurada en el estilo inventado por Gordon Plotkin.

TAPAS es el resultado de un trabajo colectivo iniciado en 1990 con una herramienta denominada JACK por el IEI CNR de Pisa . [1] El trabajo fue continuado por el ISTI - CNR de Pisa . La nueva versión de TAPAS fue desarrollada en el Dipartimento Sistemi ed Informatica de la Universidad de Florencia .

Véase también

Referencias

  1. ^ Página web de JACK (Just Another Cuncurrency Kit)

Enlaces externos