A framework for the specification and validation of Real Time Systems using Circus Action / A framework for the specification and validation of Real Time Systems using Circus Action

AUTOR(ES)
DATA DE PUBLICAÇÃO

2006

RESUMO

Circus à uma linguagem de especificaÃÃo e programaÃÃo que combina CSP, Z, e construtores do CÃlculo de Refinamento. A semÃntica de Circus està baseada na Unifying Theories of Programming (UTP). Neste trabalho estendemos um subconjunto de Circus com operadores de tempo. A nova linguagem à denominada de Circus Time Action. Propomos um modelo novo do tempo que estende o modelo da UTP, adicionando variÃveis de observacÃo para registrar a passagem de tempo. O novo modelo à usado para dar a semÃntica formal de Circus Time Action. Propriedades algÃbricas do modelo original de Circus sÃo validadas no novo modelo; propriedades novas sÃo exploradas e validadas dentro do contexto de Circus Time Action. A vantagem de utilizar o padrÃo de unificaÃÃo proposto pela UTP à poder comparar e relacionar diferentes modelos. Definimos uma funÃÃo de abstraÃÃo, L, que faz o mapeamento das observaÃÃes registradas no novo modelo (com tempo) para observaÃÃes no modelo original (sem tempo); uma funÃÃo inversa, R, à tambÃm definida. O objetivo à estabelecer uma ligaÃÃo formal entre o modelo novo com tempo e o modelo original da UTP. A funÃÃoo L e sua funÃÃo inversa R formam uma conexÃo de Galois. Usando a funÃÃo de abstraÃÃo, nÃs introduzimos a definiÃÃo de programas insensÃveis ao tempo. A funÃÃo de abstraÃÃo permite a exploraÃÃo de algumas propriedades nÃo temporais de um programa. Apresentamos um exemplo simples para ilustrar o uso da funÃÃo de abstraÃÃo na validaÃÃo de propriedades que nÃo tÃm tempo associado. Entretanto, sistemas de tempo real tÃm requisitos temporais que necessitam ser validados. Neste sentido, propomos um framework para a validaÃÃo de requisitos nÃo temporais usando os dois modelos e a relaÃÃo entre eles. A estrutura do framework à baseada em um processo de particionamento. Tendo como ponto de partida o programa e sua especificaÃÃo escritos em Circus Time Action, aplicamos uma funÃÃo sintÃtica que gera uma forma normal do programa e sua especificaÃÃo. A forma normal consiste de duas partes: a primeira à um programa sem operadores de tempo, mas com eventos que, por convenÃÃo, representam aÃÃes temporais; a segunda à uma coleÃÃo de temporizadores (timers) usados pelo programa. A composiÃÃo paralela de ambas as partes à semanticamente equivalente ao programa original. Usando apenas o componente da forma normal que nÃo envolve tempo explicitamente, mostramos que à possÃvel raciocinar sobre propriedades de tempo no modelo nÃo temporal; provamos formalmente a validade deste resultado. Para ilustrar o uso do framework, utilizamos um sistema de alarme simplificado como estudo de caso. Como a validaÃÃo à reduzida ao modelo sem tempo, usamos a ferramenta de verficaÃÃo de modelos de CSP (FDR) para realizar as provas mecanicamente. Esta à uma outra contribuiÃÃo importante deste trabalho

ASSUNTO(S)

utp (unifying theories of programming) - real time model - prova formal ciencia da computacao mÃtodos formais - especificaÃÃo e validaÃÃo engenharia de software

ACESSO AO ARTIGO

Documentos Relacionados