Tiempo Lógico @ Trabajo para el Modelado y Análisis de Sistemas Embebidos

El tiempo lógico es una forma relajada de tiempo promovida por lenguajes sincrónicos que es funcional, elástica (puede ser abstraída o refinada) y multiforme. Todas estas propiedades hacen que el tiempo lógico sea adecuado también en el tiempo de diseño, mientras que las anotaciones precisas de tiempo físico sólo deberían importar en las etapas posteriores a la síntesis. El Lenguaje de Especificación de Restricciones del Reloj (CCSL) es un lenguaje concreto dedicado a la modelización y análisis de las propiedades del tiempo lógico. El CCSL se definió inicialmente como un compañero para el modelo de tiempo del perfil UML para MARTE. Ahora se ha convertido en un lenguaje de modelado de dominio específico para capturar relaciones causales, cronológicas y temporales. Debe complementar otros modelos sintácticos para capturar su modelo de cálculo subyacente. Este libro comienza describiendo los modelos históricos de concurrencia que han inspirado la construcción de CCSL. Luego, CCSL se introduce y se utiliza para construir bibliotecas dedicadas a dos modelos estándar emergentes de los dominios automotriz (East-ADL) y aviónico (AADL). Por último, se presenta una técnica basada en la observación para verificar las implementaciones de Esterel y VHDL con respecto a las especificaciones del CCSL.