Tempo Lógico @ Trabalho para a Modelação e Análise de Sistemas Embebidos

O tempo lógico é uma forma relaxada de tempo promovida por linguagens síncronas que é funcional, elástica (pode ser abstraída ou refinada), e multiforme. Todas estas propriedades tornam o tempo lógico adequado também no tempo de concepção, enquanto que as anotações de tempo físico precisas só devem ter importância em fases posteriores de pós-síntese. A Clock Constraint Specification Language (CCSL) é uma linguagem concreta dedicada à modelação e análise das propriedades lógicas do tempo. A CCSL foi inicialmente definida como uma companheira para o modelo temporal do perfil UML para a MARTE. Tornou-se agora uma linguagem de modelação de domínio específico para a captura de relações causais, cronológicas e temporais. Deve complementar outros modelos sintácticos para captar o seu modelo de cálculo subjacente. Este livro começa por descrever os modelos históricos de concurrência que inspiraram a construção do CCSL. Em seguida, o CCSL é introduzido e utilizado para construir bibliotecas dedicadas a dois modelos padrão emergentes dos domínios automóvel (East-ADL) e aviónico (AADL). Finalmente, é apresentada uma técnica baseada em observadores para verificar as implementações de Esterel e VHDL em relação às especificações CCSL.